Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Altenkirch, Thorsten (Επιμελητής έκδοσης), McBride, Conor (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
Σειρά:Lecture Notes in Computer Science, 4502
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
  • Crafting a Proof Assistant
  • On Constructive Cut Admissibility in Deduction Modulo
  • Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
  • Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
  • Deciding Equality in the Constructor Theory
  • A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
  • Truth Values Algebras and Proof Normalization
  • Curry-Style Types for Nominal Terms
  • (In)consistency of Extensions of Higher Order Logic and Type Theory
  • Constructive Type Classes in Isabelle
  • Zermelo’s Well-Ordering Theorem in Type Theory
  • A Finite First-Order Theory of Classes
  • Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
  • Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs
  • Subset Coercions in Coq
  • A Certified Distributed Security Logic for Authorizing Code.