A Type Soundness Proof for the Polymorphic λ-Calculus with References

Lam-Ref Example version 0.3

About

We design and prove the soundness of a sophisticated type system for a Curry-style lambda calculus with references.  The type system include not only basic types such as nat and functions, but also key historically troublesome types such as impredicative quantified types, contravariant equirecursive types, and reference types.  We prove the standard typing rules as lemmas from our semantic definitions, and show how to type a variety of interesting programs with our typing rules.

Note: We are planning some human-readable documentation.  For now, see our POPL10 paper, our APLAS tutorial, and this web site.

This example is designed to showcase some of the features of the Mechanized Semantic Library, particularly the Indirection Theory and Logics components.  It is distributed with the MSL under the same BSD-style license.

Component Overview

# Name Description
1. Setup Engineering to handle files in multiple directories (for Proof General)
2. Trusted Computing Base Definition of the syntax and operational semantics of the machine; that is, everything needed to understand the statement of the safety property
3. Machine Definitions and lemmas about the operational semantics (mostly substitution and evaluation)
4. Type System Semantic definitions of types; statement of the typing rules and their soundness proofs; the proof of the safety theorem
5. Programs Examples of programs that we can type; proof of unsoundness of unrestricted universals

File list

# File name Line Count     Component
1. setup.v 6   Setup
2. lam_ref_tcb.v 182   Trusted Computing Base
3. lam_ref_mach_defs.v 110   Machine
4. lam_ref_mach_lemmas.v 696   Machine
5. lam_ref_eval.v 180   Machine
6. lam_ref_type_prelim.v 604   Type System
7. lam_ref_type_defs.v 564   Type System
8. lam_ref_type_safety.v 128   Type System
9. lam_ref_type_lemmas.v 894   Type System
10. lam_ref_type_rules.v 932   Type System
11. programs.v 439   Programs
12. crash.v 259   Programs
         
  Total 4,994    

Component Details

Setup

Download setup.v
An engineering hack to help Proof General handle files in multiple directories.

Trusted Computing Base

Download lam_ref_tcb.v
Definition of the syntax and operational semantics of the machine; that is, everything needed to understand the statement of the safety property.  At the end we will produce a proof of this property for a particular program; since the definition of safety is both simple and stated in standard form, we know that at the end of the day we have proved something nontrivial.

Machine

Download lam_ref_mach_defs.v
Supplementary definitions about the machine that were not on the critical path to defining safety, such as: custom tactics, coercions, environment substitutions, and machine execution.

Download lam_ref_mach_lemmas.v
Lemmas about the lambda calculus with references that do not depend on the type system for their statement or proof, such as: decidability, substitution, closedness, determinism, etc.

Download lam_ref_eval.v
An evaluator for the lambda calculus with references, together with its correctness proof.

Type System

Download lam_ref_type_prelim.v
Instantiate the knot of indirection theory, define the "extendedly" relation, and prove basic facts about it.  Various utility lemmas.

Download lam_ref_type_defs.v
Definition of the type constructors and their proof of heredity.  Proofs about subtyping and contractiveness of the constructors.

Download
lam_ref_type_safety.v
A proof that well-typed programs are safe in the sense defined in the trusted computing base.

Download
lam_ref_type_lemmas.v
Utility lemmas for the type system and preservation of types under the redexes.

Download lam_ref_type_rules.v
Proof of the soundness of the standard typing rules of the polymorphic lambda calculus with references.

Programs

Download programs.v
Demonstrations that we can type interesting programs using our typing rules, including: the Church booleans, Church option type, the standard diverging term ((λx. x x)(λx. x x)), the call-by-value fixpoint combinator, Landin's knot, and the factorial program.  We also prove that every untyped lambda term (that is, lambda, application, and variables) can be well-typed.

Download crash.v
Shows the unsoundness of unrestricted universal typing; the way around this problem that we use is the value restriction from ML.

People

The Mechanized Semantic Library is developed and maintained by Andrew W. Appel, Robert Dockins, and Aquinas Hobor.

License

Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

- Redistribution of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

- Redistribution in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR THE CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.