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