Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers /
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | , |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | 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.