Types for Proofs and Programs: International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007 Revised Selected Papers

This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2007, the concluding conference of the Types project, held in Cividale del Friuli, Italy, in May 2007. The 13 revised full papers presented were carefully reviewed and selected from 22 submissions. The topic of this last annual workshop of the Types Working Group was formal reasoning and computer programming based on type theory. Great importance was attached to languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalization of mathematics and mathematics education. Subject Title Page 2 Preface 5 Table of Contents 7 Algorithmic Equality in Heyting Arithmetic Modulo 8 Introduction 8 Definitions 9 Deduction Modulo 9 Theories in Natural Deduction Modulo 9 Relations between Theories 10 Models 10 Different Presentations of Heyting Arithmetic - From Axioms to Rewrite Rules 12 The Axiomatic Presentation of Heyting Arithmetic 12 $\mbox{HA}_R$, a Theory Equivalent to HA 13 $\mbox{HA}_N$, a Conservative Extension of $\mbox{HA}_R$ 14 $\mbox{HA}_K$, a Conservative Extension of $\mbox{HA}_N$ 17 $\mbox{HA}_{\Rightarrow}$, a Purely Computational Presentation of Heyting Arithmetic 19 Properties of HA_{\Rightarrow} 20 $HA_{\Rightarrow}$ Is a Conservative Extension of HA 20 Decidability of the Congruence Defined by the $HA_{\Rightarrow}$ Rewrite System 20 Cut Elimination Property 22 Discussion 23 Conclusion 23 CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types 25 Introduction 25 High-Level Structure of the Formalisation 26 Class Pools and Dynamic Loading 28 The Class Pool 28 Dynamic Class Loading 29 Writing and Proving Functions That Search the Class Pool 32 Interface to the Rest of the Formalisation 33 The Object Heap and Static Fields 34 Object Heaps 34 Static Fields 35 Modelling Execution 35 The Virtual Machine State 36 Instruction Execution 36 Extraction to O'Caml 37 Related Work 37 Conclusions 38 Dependently Sorted Logic 40 Introduction 40 Theories of Dependent Sorts 41 Expressions 41 Signatures 44 Generalised Algebraic Theories 47 Dependently Sorted Algebras 49 Completeness 50 Systems of Dependently Sorted Logic 51 Structures for Dependently Sorted Logic 54 Finiteness in a Minimalist Foundation 58 Introduction 58 Minimal Type Theory: A Brief Introduction 59 A Constructive Concept of Finiteness 61 Finite Subsets 66 Some Other Notions of Finiteness 73 A Declarative Language for the Coq Proof Assistant 76 Introduction 76 Motivations 76 Related Work 77 A New Language for the Coq Proof Assistant 77 Outline 78 Informal Description 79 An Introductory Example 79 Forward and Backward Proofs 80 Justifications 80 Partial Conclusion 81 Syntax and Semantics 83 Syntax 83 Commands Description 84 Operational Semantics 86 Proof Editing 87 Well-Formedness 87 Formal Proof Sketches 87 Conclusion 87 Further Work 87 Conclusion 88 Operational Semantic (Continued) 89 Characterising Strongly Normalising Intuitionistic Sequent Terms 92 Syntax of {\lambda^{\mathsf{Gtz}}} 93 Intersection Types for {\lambda^{\mathsf{Gtz}}} 94 Typeability $\Rightarrow$ SN 97 SN $\Rightarrow$ Typeability 99 Typeability of Normal Forms 99 Subject Expansion at Root Position 101 Generalised Applications and Explicit Substitutions 103 Conclusion 105 Intuitionistic vs. Classical Tautologies, Quantitative Comparison 107 Introduction 107 Basic Facts 108 Catalan Numbers 108 Algebraic Asymptotics 108 Bell Numbers 109 Formulas 109 Counting up to Names 109 Simple Tautologies 110 Discussion 115 In the Search of a Naive Type Theory 117 Why Not Set Theory? 117 Why Type Theory and What Type Theory? 119 Informal Exposition 122 Naive Type Theory as a Pure Type System 124 Verification of the Redecoration Algorithm for Triangular Matrices 132 Introduction 132 Triangular Matrices 133 A List-Based Model 137 Verification Against the List-Based Model 140 Details on Formal Verification with Coq 143 Details on Formal Verification with Isabelle 144 Conclusions 147 A Logic for Parametric Polymorphism with Effects 149 Introduction 149 A Type Theory for Polymorphism and Effects 150 The Logic 153 Verifying Polymorphic Type Encodings 157 Inductive and Coinductive Types 160 Working with Mathematical Structures in Type Theory 164 Introduction 164 Dependently Typed Records in Type Theory 166 $\Psi$ and $\Sigma$ Types 167 Weakly Manifest Types 168 Manifesting Coercions 168 Deep []!with! Construction 170 Nested with Contructions 171 Signature Strengthening and []!with! Commutation 171 Remarks on Code Extraction 172 Structures, Inheritance, Shared Carrier and Unification 172 Type Reconstruction with Unification and Coercions 174 Type Reconstruction Algorithm 174 Conclusions 178 On Normalization by Evaluation for Object Calculi 180 Introduction 180 Syntax and Conversion Semantics of Object Calculus 182 FM Domain Theory 183 Normalization Procedure 185 Correctness 187 Conclusion 191 Existence Proof 193 Attributive Types for Proof Erasure 195 Introduction 195 Formal Development 198 Extension 204 An Example 206 Related Work and Conclusion 208 Author Index 210 Front Matter....Pages - Algorithmic Equality in Heyting Arithmetic Modulo....Pages 1-17 CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types....Pages 18-32 Dependently Sorted Logic....Pages 33-50 Finiteness in a Minimalist Foundation....Pages 51-68 A Declarative Language for the Coq Proof Assistant....Pages 69-84 Characterising Strongly Normalising Intuitionistic Sequent Terms....Pages 85-99 Intuitionistic vs. Classical Tautologies, Quantitative Comparison....Pages 100-109 In the Search of a Naive Type Theory....Pages 110-124 Verification of the Redecoration Algorithm for Triangular Matrices....Pages 125-141 A Logic for Parametric Polymorphism with Effects....Pages 142-156 Working with Mathematical Structures in Type Theory....Pages 157-172 On Normalization by Evaluation for Object Calculi....Pages 173-187 Attributive Types for Proof Erasure....Pages 188-202 Back Matter....Pages -