Home
This project is a proof-of-concept a derivational approach to proving the equivalence of different representations of a type system.
Different ways of representing type assignments are convenient for particular applications such as reasoning or implementation, but some kind of correspondence between them should be proven. In this paper we deal with two such semantics for type checking: one, due to Kuan et al., in the form of a term rewriting system and another in the form of a traditional set of derivation rules.
By employing a set of techniques investigated by Danvy et al., we mechanically derive the correspondence between a reduction-based semantics for type-checking and a traditional one in the form of derivation rules, implemented as a recursive descent. The correspondence is established through a series of semantics-preserving functional program transformations.
Under reduction-evaluation
For more details of the derivation see the paper A correspondence between type checking via reduction and type checking via evaluation, published in Information Processing Letters, Volume 112, Issues 1–2, 15 January 2012, Pages 13–20.
or the accompanying technical report
A Correspondence between Type Checking via Reduction and Type Checking via Evaluation.
The PLT Redex implementation is available at plt-redex/type-reduction.rkt.
Under evaluation-secd
For more details of the derivation see the paper From type checking by recursive descent to type checking with an abstract machine, published at LDTA '11.
The PLT Redex implementation is available at plt-redex/type-sec-machine.rkt.
The sources are released under CRAPL license.
If you have questions or concerns about the CRAPL, or you need more information about this license, please contact Prof. Matthew Might.