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