Cited in
(55)- Eliminating dependent pattern matching without K
- I got plenty o' nuttin'
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Visible type application
- Contributions to a computational theory of policy advice and avoidability
- Exercising Nuprl's open-endedness
- Automatically proving equivalence by type-safe reflection
- Unified syntax with iso-types
- AURA
- Agda
- Cayenne
- Epigram
- Flask
- AoPA
- Mtac
- Frank
- TCB
- HoTT
- CoALP
- Koka
- Idris
- AmiCo
- TAG
- CoCaml
- cubicaltt
- Eff
- RedPRL
- F*
- Template-Coq
- Equations
- PowerPoint
- Heq
- parsec
- Shonky
- Trifecta
- cart-cube
- indentation
- The essence of ornaments
- scientific article; zbMATH DE number 7453982 (Why is no real title available?)
- Type-specialized staged programming with process separation
- Congruence closure in intensional type theory
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Integrating induction and coinduction via closure operators and proof cycles
- Validating Brouwer's continuity principle for numbers using named exceptions
- finmap
- CQL
- idris-ct
- Statebox
- Guarded dependent type theory with coinductive types
- Hammer for Coq: automation for dependent type theory
- Elaborating dependent (co)pattern matching: no pattern left behind
- Doo bee doo bee doo
- Combining proofs and programs in a dependently typed language
This page was built for software: Irdis
