Lam-Ref Example version 0.3
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.
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.
|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 name||Line Count||Component|
|2.||lam_ref_tcb.v||182||Trusted Computing Base|
An engineering hack to help Proof General handle files in multiple directories.
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.
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.
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.
An evaluator for the lambda calculus with references, together with its correctness proof.
Instantiate the knot of indirection theory, define the "extendedly" relation, and prove basic facts about it. Various utility lemmas.
Definition of the type constructors and their proof of heredity. Proofs about subtyping and contractiveness of the constructors.
A proof that well-typed programs are safe in the sense defined in the trusted computing base.
Utility lemmas for the type system and preservation of types under the redexes.
Proof of the soundness of the standard typing rules of the polymorphic lambda calculus with references.
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.
Shows the unsoundness of unrestricted universal typing; the way around this problem that we use is the value restriction from ML.
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.