The calculus of dependent lambda eliminations
From MaRDI portal
Publication:5372010
DOI10.1017/S0956796817000053zbMath1418.68038MaRDI QIDQ5372010
Publication date: 23 October 2017
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items
From realizability to induction via dependent intersection, Monotone recursive types and recursive data representations in Cedille, Quotients by Idempotent Functions in Cedille, Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Extensional models for polymorphism
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Finitely stratified polymorphism
- Safe recursion with higher types and BCK-algebra
- Realizability and Parametricity in Pure Type Systems
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- ΠΣ: Dependent Types without the Sugar
- Fibrational Induction Rules for Initial Algebras
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- The Expressiveness of Simple and Second-Order Type Structures
- Efficient self-interpretation in lambda calculus
- Self Types for Dependently Typed Lambda Encodings
- The gentle art of levitation
- Higher-order representation of substructural logics
- Parametric higher-order abstract syntax for mechanized semantics
- Cayenne—a language with dependent types
- Boxes go bananas
- Computer Science Logic
- Efficiency of lambda-encodings in total type theory
- A relationally parametric model of dependent type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Eliminating Dependent Pattern Matching
- Inductively defined types in the Calculus of Constructions
- Primitive recursion for higher-order abstract syntax
