Epigram
From MaRDI portal
Cited in
(35)- Eliminating dependent pattern matching without K
- A New Elimination Rule for the Calculus of Inductive Constructions
- Dependent Types at Work
- Program calculation in Coq
- Dependently Typed Programming Based on Automated Theorem Proving
- Heterogeneous binary random-access lists
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- A modular type-checking algorithm for type theory with singleton types and proof irrelevance
- Extracting a DPLL algorithm
- Plastic
- AURA
- Polyp
- Agda
- Cayenne
- Irdis
- Mella
- Idris
- RedPRL
- Equations
- Heq
- cart-cube
- Accelerate
- Web interfaces for proof assistants
- Recursive coalgebras from comonads
- Type-level computation using narrowing in \(\Omega\)mega
- Congruence closure in intensional type theory
- Types for Proofs and Programs
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- A tutorial implementation of a dependently typed lambda calculus
- Unifiers as equivalences: proof-relevant unification of dependently typed data
- Containers: Constructing strictly positive types
- Advanced Functional Programming
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- Combining proofs and programs in a dependently typed language
This page was built for software: Epigram
