The calculus of dependent lambda eliminations
From MaRDI portal
Publication:5372010
Recommendations
- Self types for dependently typed lambda encodings
- A tutorial implementation of a dependently typed lambda calculus
- A New Elimination Rule for the Calculus of Inductive Constructions
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- scientific article; zbMATH DE number 1405632
Cites work
- scientific article; zbMATH DE number 1722653 (Why is no real title available?)
- scientific article; zbMATH DE number 1722663 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1302059 (Why is no real title available?)
- scientific article; zbMATH DE number 1354162 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A relationally parametric model of dependent type theory
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
- Cayenne -- a language with dependent types
- Computer Science Logic
- Efficiency of lambda-encodings in total type theory
- Efficient self-interpretation in lambda calculus
- Eliminating Dependent Pattern Matching
- Extensional models for polymorphism
- Fibrational induction rules for initial algebras
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- Finitely stratified polymorphism
- Higher-order representation of substructural logics
- Homotopy type theory. Univalent foundations of mathematics
- Inductively defined types in the Calculus of Constructions
- Internalizing relational parametricity in the extensional calculus of constructions
- Parametric higher-order abstract syntax for mechanized semantics
- Primitive recursion for higher-order abstract syntax
- Realizability and parametricity in pure type systems
- Safe recursion with higher types and BCK-algebra
- Self types for dependently typed lambda encodings
- The Expressiveness of Simple and Second-Order Type Structures
- The gentle art of levitation
- \(\Pi \Sigma \): dependent types without the sugar
Cited in
(12)- A New Elimination Rule for the Calculus of Inductive Constructions
- Self types for dependently typed lambda encodings
- The Lambek calculus with iteration: two variants
- scientific article; zbMATH DE number 1763413 (Why is no real title available?)
- Quotients by idempotent functions in Cedille
- Impredicative encodings of inductive-inductive data in Cedille
- From realizability to induction via dependent intersection
- A dependent dependency calculus
- Cut elimination for a calculus with context-dependent rules
- A tutorial implementation of a dependently typed lambda calculus
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- Monotone recursive types and recursive data representations in Cedille
This page was built for publication: The calculus of dependent lambda eliminations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5372010)
