Introduction to Type Theory

DOI10.1007/978-3-642-03153-3_1zbMath1250.68088OpenAlexW2160076872MaRDI QIDQ5191087

Herman Geuvers

Publication date: 28 July 2009

Published in: Language Engineering and Rigorous Software Development (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03153-3_1

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (2)

A symbolic transformation language and its application to a multiscale method ⋮ The correctness of Newman's typability algorithm and some of its extensions

Uses Software

• Coq
• ML
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Functorial polymorphism
• Combinatory logic. With two sections by William Craig.
• Lectures on the Curry-Howard isomorphism
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The system \({\mathcal F}\) of variable types, fifteen years later
• The lambda calculus, its syntax and semantics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• A theory of type polymorphism in programming
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Comparing cubes of typed and type assignment systems
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• A simple proof of the undecidability of inhabitation in λP
• A framework for defining logics
• Definierbare Funktionen imλ-Kalkül mit Typen
• Collections, sets and types
• Some logical and syntactical observations concerning the first-order dependent type system λP
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic
• A formulation of the simple theory of types

This page was built for publication: Introduction to Type Theory