A brief history of value restriction

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

Table of contents

1 From Programming to Program Proving
1.1 Writing functional programs
1.2 Proofs of ML programs
1.3 A brief history of value restriction
1.4 Dependent functions and relaxed restriction
1.5 Handling undecidability
1.6 Related work and similar systems
1.7 Thesis overview
2 Untyped calculus and abstract machine
2.1 The pure -calculus
2.2 Evaluation contexts and reduction
2.3 Call-by-value Krivine machine
2.4 Computational e|fects and -calculus
2.5 Full syntax and operational semantics
2.6 Classi{cation of processes
3 Observational equivalence of programs
3.1 Equivalence relation and properties
3.2 Compatible equivalence relations
3.3 Equivalences from reduction
3.4 Inequivalences from counter-examples
3.5 Canonical values
4 Types and realizability semantics
4.1 Observational equivalence type
4.2 Quanti{cation and membership type
4.3 Sorts and higher-order types
4.4 Typing judgments for values and terms
4.5 Call-by-value realizability semantics
4.6 Adequacy
4.7 Typing stacks
5 A model for a semantical value restriction
5.1 Dependent function types
5.2 The limits of the value restriction
5.3 Semantical value restriction
5.4 Semantics for semantical value restriction
5.5 Final instance of our model
5.6 Derived type system
5.7 Understanding our new equivalence
6 Introducing subtyping into the system
6.1 Interests of subtyping
6.2 Symbolic witnesses and local subtyping
6.3 Typing and subtyping rules
6.4 Semantics of subtyping
6.5 Completeness on pure data types
6.6 Normalisation, safety and consistency
6.7 Toward (co-)inductive types and recursion
7 Implementation and examples
7.1 Concrete syntax and syntactic sugars
7.2 Encoding of strict product types
7.3 Booleans and tautologies
7.4 Unary natural numbers and totality
7.5 Lists and their vector subtypes
7.6 Sorted lists and insertion sort
7.7 Lookup function with an exception
7.8 An in{nite tape lemma on streams
References