swMATH9687MaRDI QIDQ21666FDOQ21666
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/11546382_3
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
- Heterogeneous binary random-access lists
- Dependently Typed Programming Based on Automated Theorem Proving
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- A modular type-checking algorithm for type theory with singleton types and proof irrelevance
- Extracting a DPLL algorithm
- Web interfaces for proof assistants
- Plastic
- Type-level computation using narrowing in \(\Omega\)mega
- Recursive coalgebras from comonads
- AURA
- Polyp
- Agda
- Cayenne
- Irdis
- Mella
- Congruence closure in intensional type theory
- Idris
- RedPRL
- Equations
- Heq
- cart-cube
- 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
- Accelerate
- 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
