tps : eval E E' -> of E T -> of E' T -> type.
%mode tps +R +P -Q.
- : tps (eval1 PR PF) PTE (PF' _ PTR')
<- tpsfocus PF PTE PTR PF'
<- tpsrdx PR PTR PTR'.
%worlds () (tps D P _).
%total D (tps D P _).
and the key progress lemma, if a focusable expression has a type it can be reduced, fprog : focus E PPV C -> of E T -> eval E E' -> type.
%mode fprog +F +P -D.
- : fprog (PF : focus E PPV _) PT (eval1 R PF)
<- tpsfocus PF PT PTPV _
<- typed-preval PPV PTPV R.
%worlds () (fprog _ _ _).
%total {} (fprog _ _ _).
share the same lemma tpsfocus -- asserting that if an expression is well-typed then the result of its focusing is well-typed. Evaluation contexts are modeled as meta-level functions.Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness
Information and Computation, v115, N1, pp. 38-94, 1994
Our broad goal is designing a trusted kernel to statically assure safety of a (recursive, multi-level) critical section: the program may re-enter the critical section but must not execute any blocking operation until it fully exited the critical section. To prove that the trusted kernel enforces the yield property we extend our previous syntactic proof for empty-list and array-bound checking: We define a language Strict with a sound type system, then show that any well-typed program in Lax (an idealization of Haskell) that uses only the exported names from the trusted kernel is a translation of a well-typed Strict program.
Our language Strict extends System F with a family of monads mn , one for each natural number n (an interrupt level). To the standard expressions of System F we add do and ret and special operations disable and yield . The latter corresponds to a blocking operation; disable e executes e in a critical section with the interrupts disabled by one level.
The dynamic semantics of Strict is formulated in terms of two mutually recursive reduction functions. The simplification function reduces terms; it is the standard call-by-name reduction of System F terms. The execution function operates on configurations <n,e> where n is the interrupt level and e is a term (of a monadic type). This distinction between two reduction relations is characteristic of monadic metalanguages.
The execution of disable and yield changes and checks the interrupt level. Accordingly, these constructs call for the only typing rules not standard for System F and monads. Not coincidentally, it is these typing rules that assure the yield property. Our mechanized proof of type preservation and progress essentially verifies that the typing rules match the dynamic semantics for disable and yield .
Using Twelf, we demonstrate the fully worked-out formal semantics of Strict and the complete formal proofs of type preservation and progress. Since we have two evaluation relations -- simplification and execution, corresponding to the two levels of the language -- we have to prove progress and preservation for both.
Our semantics is essentially small step, but with an implicit context: we keep focusing until we hit a redex. Our formalized semantics is distinguished from many other formalizations in Twelf by the following features. First, the rules of our reduction relations are free from overlapping (which makes the semantics deterministic). Second, the small-step semantics (albeit more involved than the big-step semantics shown for mini-ML and other examples in the Twelf distribution) gives meaningful progress theorems. Many Twelf formalizations do not distinguish well-typed divergent terms from ill-typed ones: both lead to non-terminating reductions. In contrast, in our dynamic semantics non-sensical terms do get stuck rather than diverge; we prove that well-typed terms do not get stuck.
Joint work with Chung-chieh Shan.
E. Moggi and S. Fagorzi. A Monadic Multi-stage Metalanguage. FoSSaCS 2003
Hao Chen and Jonathan S. Shapiro. Using Build-Integrated Static Checking to Preserve Correctness Invariants. CCS'04: Proc. 11th ACM conf. on Computer and Communications Security, pp 288-297, 2004.
The paper describes the application of the finite-state model checker MOPS to assure safety properties in the operating system kernel EROS. One of such properties is the `yield' property: the kernel must not call yield() when interrupts are disabled. EROS permits disabling interrupts by multiple levels, that is, multiple times in succession; each disabling must be balanced by exactly one enabling. This corresponds to so-called recursive locks. One may acquire the same lock multiple times, but then one must release it that many times: lock acquisitions and releases must be properly nested. Safe control flows with recursive locks cannot be modeled by a finite-state machine. In order to use MOPS, the authors had to introduce an approximation and limit the recursion depth, to 5.
Lightweight static capabilities
Explanation of the trusted kernel approach to static safety and of the method to prove its soundness.
When implementing a DSL in a host language, we need to encode not only DSL terms but also their semantics. The latter often takes form of a definitional interpreter for the DSL written in the host language. Operational semantics, a mapping from terms to terms, can be encoded as the meta-language function eval . An intrinsic encoding again lets us enforce invariants: A reduction rule that fails the invariant cannot even be defined. A useful invariant to encode is subject reduction: eval preserves DSL types of the evaluated expressions. The progress property -- every well-typed non-value can be reduced -- can also be represented in the encoding, a bit less directly. Intrinsic encodings thus greatly simplify meta-theoretic proofs such as type soundness.
For example, we define (in Twelf) one-step reduction as:
eval : {E:exp T} non-value E -> exp T -> type.
That definition itself is the statement of subject reduction: any expression E of type T that is not a value is reduced to an expression of the same type T. Furthermore, eval is total: every non-value can be further reduced. This is the statement of progress. We supply the totality declaration, and Twelf agrees.Thanks to Robert Harper, Dan Licata, William Lovas and Tom Murphy for helpful discussions about the intrinsic encoding. Thanks to Chung-chieh Shan for pointing out the connection between tagless final DSL embeddings and intrinsic encodings in Twelf.
tagless-l.elf [8K]
Intrinsic, higher-order abstract syntax encoding of simply-typed call-by-value lambda-calculus with integers, arithmetic, and fix-point. The dynamic semantics is small step, with no explicit contexts: neither on the object level, nor on the meta-level (All world declarations are empty). This Twelf code defines the evaluator and the mechanized proofs of type soundness (subject reduction and progress). The style of proofs in this file is used to prove type soundness of the calculus with shift/reset and effect typing.
< http://twelf.plparty.org/wiki/Summer_school_2008 >
Specifically, Class 3: Type safety for MinML (intrinsic encoding)
Frank Pfenning: `Church and Curry: Combining Intrinsic and Extrinsic Typing'
< http://www.cs.cmu.edu/~fp/papers/andrews08.pdf >
An insightful exposition of intrinsic typing and applications
a->b but rather a/t1->b/t2 , so to describe effects that may occur when the function is applied. Despite the more complex expression and arrow types, all types are inferred and no type annotations are required. This is joint work with Kenichi Asai, Noriko Hirota, Yukiyoshi Kameyama and Chung-chieh Shan.One mechanized soundness proof is done in Coq with a locally nameless methodology. The calculus includes the let-bound polymorphism but omits, for simplicity, the fixpoint and constants. This development deals only with meta-theory: it proves subject reduction and progress properties, but does not infer types and does not evaluate expressions.
We have also mechanized type soundness in Twelf, using the intrinsic encoding of the calculus. We present not only progress and subject reduction proofs but also the type inferencer and the evaluator: we can run sample terms and see their types. Our code includes the standard shift/reset test suite. It is Twelf itself that infers and checks object language types. We did not specify the type-checking relation since terms not typeable in the object language cannot be built. More remarkably, the one-step evaluator of our calculus is also the proof term of type soundness. In other words, the very proof of type soundness can be used to evaluate sample expressions. Proofs literally have a practical use.
tagless-dl.elf [14K]
The Twelf development
README.dr [2K]
The Isabelle/HOL development by Kenichi Asai, Ochanomizu University, 2005.
He has formalized Danvy/Filinski calculus with the type-and-effect system, without let-polymorphism. He has proved subject reduction.
Joint work with Yukiyoshi Kameyama and Chung-chieh Shan.
wmm-talk-notes.pdf [146K]
The annotated slides of the talk presented at the 5th ACM SIGPLAN Workshop on Mechanizing Metatheory. September 25, 2010. Baltimore, Maryland.
circle-shift-1.elf [50K]
Warm-up: two-stage lambda calculus with delimited control effects
This Twelf code defines the calculus, specifies its static and dynamic semantics, and proves the type soundness. The code contains many examples, including the staged Gibonacci example with memoization and let-insertion.
circle-shift-n.elf [48K]
Multi-staged calculus with delimited control
This is the main development, for arbitrarily many stages, described in the talk and the abstract.
The article on the Twelf Wiki shows an example requiring strengthening and describes one solution, which relies on defining term equality. In this article we demonstrate simpler examples of strengthening, and two surprisingly trivial solutions. Quite literally, one solution deals with the problem head-on, whereas the second one avoids the problem in a round-about way. The examples are inspired by staging calculi. At the end we describe the real development, which gives perhaps the first formal proof of type preservation of primitive reductions in an expressive staged calculus with escapes, run and cross-staged persistence. The type-preservation proof uses both of our solutions and requires two strengthening lemmas. Throughout we use Twelf and the higher-order abstract syntax (HOAS) for terms, without ever resorting to concrete syntax for `variables'.
< http://twelf.plparty.org/wiki/Strengthening >
The Twelf Project: the tutorial on Strengthening
The running example is proving that evaluation in the language with locations preserves the well-formedness of terms with respect to the store (no dangling references or loops).
strengthen.elf [7K]
Twelf code demonstrating a simple example of the strengthening problem and showing two surprisingly simple solutions
translation-problem.elf [7K]
More realistic example of strengthening, when proving totality or other meta-theoretical property of a translation from one higher-order abstract syntax expression to another
Two-level staged calculus with environment classifiers, run and cross-stage persistence
Twelf formalization of the two-level call-by-value calculus based on lambda-a of Taha and Nielsen's ``Environment Classifiers'' (POPL03).
We mechanically prove that any non-value term can be decomposed into a possibly open pre-value and the possibly binding context. We prove type preservation of primitive reductions.
A good example is McCarthy's function 91:
f91(n,k) = if k <= n then n else f91(f91(n+1,k),k)It is straightforward to implement in Twelf. Since the function is not obviously structurally recursive, proving its termination requires advanced reasoning, beyond the abilities of the termination checker. We demonstrate how to do this advanced reasoning and so convince Twelf the function is terminating -- without changing the definition of the function.
We end up proving a stronger result about the function: for all natural numbers i and n , f91(n,i+n) = i+n . We state this property and constructively prove it in Twelf. The proof relies on the lexicographic structural recursion and ex falso quodlibet.
proving-f91.elf [6K]
The complete commented Twelf development.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML