Epigram
From MaRDI portal
Software:21666
swMATH9687MaRDI QIDQ21666FDOQ21666
Author name not available (Why is that?)
Cited In (22)
- Eliminating dependent pattern matching without K
- A New Elimination Rule for the Calculus of Inductive Constructions
- Dependent Types at Work
- Heterogeneous binary random-access lists
- Dependently Typed Programming Based on Automated Theorem Proving
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- Program Calculation in Coq
- Web interfaces for proof assistants
- Type-level computation using narrowing in \(\Omega\)mega
- Recursive coalgebras from comonads
- Types for Proofs and Programs
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Unifiers as equivalences: proof-relevant unification of dependently typed data
- A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Containers: Constructing strictly positive types
- Extracting a DPLL Algorithm
- Advanced Functional Programming
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Congruence Closure in Intensional Type Theory
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- A Tutorial Implementation of a Dependently Typed Lambda Calculus
- Combining proofs and programs in a dependently typed language
This page was built for software: Epigram
