Pure Type System in Natural Deduction

For more info about our services contact : help@bestpfe.com

Table of contents

I Introduction 
1 Type systems in a nutshell
1.1 The general setting
1.2 The purpose of programming languages
1.3 A practical example
1.4 Computation on types
1.5 Where to go next ?
II Untyped equality 
2 Pure Type Systems
2.1 Pure Type System in Natural Deduction
2.1.1 Terms and Untyped Reductions
2.1.2 Presentation of Pure Type Systems
2.2 Pure Type Systems in Sequent Calculus
2.2.1 Terms and Reduction
2.2.2 Confluence of β-reduction in λ
2.2.3 Typing Rules
2.2.4 Properties of the system
2.3 Delayed Pure Type System in Sequent Calculus
2.3.1 Typing Rules
2.3.2 Properties of the system
2.4 Expansion Postponement in Delayed System
2.4.1 Postponement in Sequent Calculus
2.4.2 Postponement in Natural Deduction
2.5 Sequent Calculus and Type Inference
2.6 A brief look back at syntactical Pure Type Systems
III Typed equality 
3 Judgmental Equality
3.1 PTSs with Judgmental Equality
3.1.1 Typing Rules
3.1.2 Subject Reduction and Equivalence
3.2 Basic meta-theory of the annotated system
3.2.1 Definition of PTSs with Annotated Type Reduction
3.2.2 General properties of PTSatr
3.2.3 The Church-Rosser Property in PTSatr
3.2.4 Consequences of the Church-Rosser property
3.3 Equivalence of PTSatr and PTSs
3.3.1 Confluence of the annotation process
3.3.2 Consequences of the Erased Confluence
3.3.3 Consequences of the equivalence
4 Formalization in Coq
4.1 Formal proof: paper or computer ?
4.1.1 What is a formal proof ?
4.1.2 Automatic resolution and induction schemes
4.2 Encoding PTSs in a proof assistant
4.2.1 Questions about encodings of binders
4.2.2 Higher order encodings
4.2.3 Our final choice: de Bruijn indices
IV Conclusion and Further Research 
5 Extensions of PTS
5.1 Sorts, order and subtyping
5.2 Toward a typed conversion for CC!
5.2.1 The straightforward approach
5.2.2 Other attempts and possible leads
5.3 Other leads for future investigations