The calculus of dependent lambda eliminations
From MaRDI portal
Publication:5372010
DOI10.1017/S0956796817000053zbMATH Open1418.68038MaRDI QIDQ5372010FDOQ5372010
Authors: Aaron Stump 
Publication date: 23 October 2017
Published in: Journal of Functional Programming (Search for Journal in Brave)
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Safe recursion with higher types and BCK-algebra
- Title not available (Why is that?)
- Homotopy type theory. Univalent foundations of mathematics
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Efficient self-interpretation in lambda calculus
- Title not available (Why is that?)
- Finitely stratified polymorphism
- Parametric higher-order abstract syntax for mechanized semantics
- Primitive recursion for higher-order abstract syntax
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- The Expressiveness of Simple and Second-Order Type Structures
- Extensional models for polymorphism
- Computer Science Logic
- Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
- Title not available (Why is that?)
- Inductively defined types in the Calculus of Constructions
- Internalizing relational parametricity in the extensional calculus of constructions
- Title not available (Why is that?)
- Eliminating Dependent Pattern Matching
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- \(\Pi \Sigma \): dependent types without the sugar
- Fibrational induction rules for initial algebras
- A relationally parametric model of dependent type theory
- Title not available (Why is that?)
- The gentle art of levitation
- Efficiency of lambda-encodings in total type theory
- Higher-order representation of substructural logics
- Cayenne -- a language with dependent types
- Realizability and parametricity in pure type systems
- Self types for dependently typed lambda encodings
Cited In (12)
- Self types for dependently typed lambda encodings
- A New Elimination Rule for the Calculus of Inductive Constructions
- From realizability to induction via dependent intersection
- Cut elimination for a calculus with context-dependent rules
- Quotients by idempotent functions in Cedille
- A tutorial implementation of a dependently typed lambda calculus
- A dependent dependency calculus
- The Lambek calculus with iteration: two variants
- Title not available (Why is that?)
- Impredicative encodings of inductive-inductive data in Cedille
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- Monotone recursive types and recursive data representations in Cedille
Uses Software
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)
