Telescopic mappings in typed lambda calculus

DOI10.1016/0890-5401(91)90066-BMaRDI QIDQ757027zbMATH OpenFDO

Authors N. G. de Bruijn

Publication date 1991

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0890-5401(91)90066-B

zbMATH Keywords

lambda calculustelescopestyping

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Theory of programming languages (68N15)

Cites work

• scientific article; zbMATH DE number 4191138 (Why is no real title available?)
• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 4058907 (Why is no real title available?)
• scientific article; zbMATH DE number 4061195 (Why is no real title available?)
• scientific article; zbMATH DE number 3657156 (Why is no real title available?)
• scientific article; zbMATH DE number 3681164 (Why is no real title available?)
• scientific article; zbMATH DE number 3684935 (Why is no real title available?)
• scientific article; zbMATH DE number 3895060 (Why is no real title available?)
• scientific article; zbMATH DE number 3331288 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• The calculus of constructions

Cited in

(15)

• A minimalist two-level foundation for constructive mathematics
• An intuitionistic theory of types with assumptions of high-arity variables
• Inductive families
• Joyal's arithmetic universes via type theory
• A unified treatment of syntax with binders
• Packaging Mathematical Structures
• Two-dimensional models of type theory
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• Validating Mathematical Structures
• Elaborating dependent (co)pattern matching: no pattern left behind
• Topological quantum gates in homotopy type theory
• Dependent type refinements for futures
• Mathematical structures in dependent type theory (invited talk)
• Isomorphism is equality
• The identity type weak factorisation system

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Telescopic mappings in typed lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q757027)