Name
Abstract | ||
|---|---|---|
Expansion is an operation on typings pairs of type environments and result types in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a λ-term in systems with intersection types. This paper aims to clarify expansion and make it more accessible to a wider community by isolating the pure notion of expansion on its own, independent of type systems and types, and thereby make it easier for non-specialists to obtain type inference with flexible precision by making use of theory and techniques that were originally developed for intersection types. We redefine expansion as a simple algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple axioms and axiom schemas: the 3 standard axioms of a monoid, 4 standard axioms or axiom schemas of substitutions including one that corresponds to the usual “substitution lemma” that composes substitutions, and 1 very simple axiom schema for expansion itself. Many of the results on the algebra have also been formally checked with the Coq proof assistant. We then take System E, a λ-calculus type system with intersection types and expansion variables, and redefine it using the expansion algebra, thereby demonstrating how a single uniform notion of expansion can operate on both typings and proofs. Because we present a simplified version of System E omitting many features, this may be independently useful for those seeking an easier-to-comprehend version. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.3233/FI-2012-771 | Fundam. Inform. |
Keywords | Field | DocType |
expansion algebra,expansion variable,system e,axiom schema,result type,type environment,standard axiom,type system,intersection type,calculus type system,canonical form | Simple algebra,Axiom schema,Discrete mathematics,Combinatorics,Algebra,Axiom,Type inference,Mathematical proof,Monoid,Filtered algebra,Mathematics,Proof assistant | Journal |
Volume | Issue | ISSN |
121 | 1-4 | 0169-2968 |
Citations | PageRank | References |
2 | 0.39 | 18 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sébastien Carlier | 1 | 28 | 2.64 |
| J. B. Wells | 2 | 398 | 25.09 |