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.