Epigram
From MaRDI portal
Software:21666
No author found.
Related Items (22)
Extracting a DPLL Algorithm ⋮ Dependently Typed Programming Based on Automated Theorem Proving ⋮ Advanced Functional Programming ⋮ Heterogeneous binary random-access lists ⋮ Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory ⋮ Eliminating dependent pattern matching without K ⋮ 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 ⋮ Combining proofs and programs in a dependently typed language ⋮ Recursive coalgebras from comonads ⋮ Dependent Types at Work ⋮ Program Calculation in Coq ⋮ A UNIVERSE OF STRICTLY POSITIVE FAMILIES ⋮ Congruence Closure in Intensional Type Theory ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ A New Elimination Rule for the Calculus of Inductive Constructions ⋮ Types for Proofs and Programs ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ Containers: Constructing strictly positive types ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ Web Interfaces for Proof Assistants
This page was built for software: Epigram
