Introduction to generalized type systems

AbstractProgramming languages often come with type systems. Some of these are simple, others are sophisticated. As a stylistic representation of types in programming languages several versions of typed lambda calculus are studied. During the last 20 years many of these systems have appeared, so there is some need of classification. Working towards a taxonomy, Barendregt (1991) gives a fine-structure of the theory of constructions (Coquand and Huet 1988) in the form of a canonical cube of eight type systems ordered by inclusion. Berardi (1988) and Terlouw (1988) have independently generalized the method of constructing systems in the λ-cube. Moreover, Berardi (1988, 1990) showed that the generalized type systems are flexible enough to describe many logical systems. In that way the well-knownpropositions-as-typesinterpretation obtains a nice canonical form.

Download Full-text

Linearization of the lambda-calculus and its relation with intersection type systems

Journal of Functional Programming ◽

10.1017/s0956796803004970 ◽

2004 ◽

Vol 14 (5) ◽

pp. 519-546 ◽

Cited By ~ 5

Author(s):

MÁRIO FLORIDO ◽

LUÍS DAMAS

Keyword(s):

Programming Languages ◽

Functional Programming ◽

Type System ◽

Lambda Calculus ◽

Type Systems ◽

Functional Programming Languages

In this paper we present a notion of expansion of a term in the lambda-calculus which transforms terms into linear terms. This transformation replaces each occurrence of a variable in the original term by a fresh variable taking into account non-trivial implications in the structure of the term caused by these simple replacements. We prove that the class of terms which can be expanded is the same of terms typable in an Intersection Type System, i.e. the strongly normalizable terms. We then show that expansion is preserved by weak-head reduction, the reduction considered by functional programming languages.

Download Full-text

Using Vampire in Soundness Proofs of Type Systems

10.29007/22x6 ◽

2018 ◽

Author(s):

Sylvia Grewe ◽

Sebastian Erdweg ◽

Mira Mezini

Keyword(s):

Programming Languages ◽

Type System ◽

Lambda Calculus ◽

Type Systems ◽

Current Approach ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Domain Specific ◽

Automated Proof

Type systems for programming languages shall detect type errors in programs before runtime. To ensure that a type system meets this requirement, its soundness must be formally verified. We aim at automating soundness proofs of type systems to facilitate the development of sound type systems for domain-specific languages.Soundness proofs for type systems typically require induction. However, many of the proofs of individual induction cases only require first-order reasoning. For the development of our workbench Veritas, we build on this observation by combining automated first-order theorem provers such as Vampire with automated proof strategies specific to type systems. In this paper, we describe how we encode type soundness proofs in first-order logic using TPTP. We show how we use Vampire to prove the soundness of type systems for the simply-typed lambda calculus and for parts of a typed SQL. We report on which parts of the proofs are handled well by Vampire, and what parts work less well with our current approach.

Download Full-text

Quantifier elimination and parametric polymorphism in programming languages

Journal of Functional Programming ◽

10.1017/s0956796800000332 ◽

1992 ◽

Vol 2 (2) ◽

pp. 213-226 ◽

Cited By ~ 4

Author(s):

Harry G. Mairson

Keyword(s):

Programming Languages ◽

Lambda Calculus ◽

Quantifier Elimination ◽

Type Inference ◽

Cut Elimination ◽

Standard Interpretation ◽

Inference Problem ◽

First Order ◽

Typed Lambda Calculus ◽

Parametric Polymorphism

AbstractWe present a simple and easy-to-understand explanation of ML type inference and parametric polymorphism within the framework of type monomorphism, as in the first order typed lambda calculus. We prove the equivalence of this system with the standard interpretation using type polymorphism, and extend the equivalence to include polymorphic fixpoints. The monomorphic interpretation gives a purely combinatorial understanding of the type inference problem, and is a classic instance of quantifier elimination, as well as an example of Gentzen-style cut elimination in the framework of the Curry-Howard propositions-as-types analogy.

Download Full-text

Decomposing typed lambda calculus into a couple of categorical programming languages

Category Theory and Computer Science - Lecture Notes in Computer Science ◽

10.1007/3-540-60164-3_28 ◽

1995 ◽

pp. 200-219 ◽

Cited By ~ 6

Author(s):

Masahito Hasegawa

Keyword(s):

Programming Languages ◽

Lambda Calculus ◽

Typed Lambda Calculus

Download Full-text

Reduction Strategies for Program Extraction

CLEI electronic journal ◽

10.19153/cleiej.6.1.2 ◽

2018 ◽

Vol 6 (1) ◽

Author(s):

Maribel Fernandez ◽

Ian Mackie ◽

Paula Severi ◽

Nora Szasz

Keyword(s):

Type System ◽

Lambda Calculus ◽

General Setting ◽

Type Systems ◽

Program Extraction ◽

Pure Type ◽

Typed Lambda Calculus ◽

Reduction Strategies ◽

Pure Type Systems ◽

Reduction Relation

We introduce Pure Type Systems with Pairs generalising earlier work on program extraction in Typed Lambda Calculus. We model the process of program extraction in these systems by means of a reduction relation called o-reduction, and give strategies for Bo-reduction which will be useful for an implementation of a proof assistant. More precisely, we give an algorithm to compute theo-normal form of a term in Pure Type System with Pairs, and show that this defines a prejection from Pure Type Systems with Pairs to standart Pure Type Systems. This result shows that o-reduction is an operational description of aprgram extraction that is independent of the particular Typed Lambda Calculus specified as a Pure Typoe System. For B-reduction, we define weak and strong reduction strategies using Interaction Nets, generalising well-know efficient strategies for the l-calculus to the general setting of Pure Type Systems.

Download Full-text