Telescopic mappings in typed lambda calculus

DOI10.1016/0890-5401(91)90066-BzbMath0723.68024MaRDI QIDQ757027

No author found.

Publication date: 1991

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

zbMATH Keywords

lambda calculustypingtelescopes

Mathematics Subject Classification ID

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

Related Items (12)

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

Uses Software

• Automath

Cites Work

• The calculus of constructions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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