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