Cited in
(95)- Eliminating dependent pattern matching without K
- The \textsc{MetaCoq} project
- Functional modelling of musical harmony: an experience report
- I got plenty o' nuttin'
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Editorial: Special issue on programming with dependent types
- Visible type application
- Contributions to a computational theory of policy advice and avoidability
- Incorporating quotation and evaluation into Church's type theory
- Exercising Nuprl's open-endedness
- Sequential decision problems, dependent types and generic solutions
- Extracting verified decision procedures: DPLL and resolution
- Automatically proving equivalence by type-safe reflection
- Unified syntax with iso-types
- Beluga
- CLEAN
- MetaPRL
- MetaOCaml
- Agda
- Cayenne
- Cyclone
- Epigram
- AoPA
- Irdis
- FoCaLiZe
- Mtac
- Aglet
- Frank
- TCB
- MathScheme
- Lean
- CoALP
- Koka
- LLFp
- AmiCo
- Calcite
- Alms
- CoCaml
- CertiCoq
- cubicaltt
- Eff
- Hazelnut
- js_of_ocaml
- Lamdu
- mbeddr
- reFLect
- TouchDevelop
- RedPRL
- HoTTSQL
- F*
- OEuf
- Template-Coq
- ELPI
- Equations
- HOL Light QE
- Rust
- Meta Dedukti
- PowerPoint
- GREEND
- Heq
- parsec
- Shonky
- Trifecta
- cart-cube
- indentation
- MetaCoq
- The essence of ornaments
- scientific article; zbMATH DE number 7453982 (Why is no real title available?)
- Tactics and certificates in Meta Dedukti
- Congruence closure in intensional type theory
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- Elaborator reflection: extending Idris in Idris
- COCHIS: stable and coherent implicits
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Biform theories: project description
- Theories as types
- Integrating induction and coinduction via closure operators and proof cycles
- Hazelnut: a bidirectionally typed structure editor calculus
- Validating Brouwer's continuity principle for numbers using named exceptions
- Bar induction is compatible with constructive type theory
- Extracting functional programs from Coq, in Coq
- A verified theorem prover backend supported by a monotonic library
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- 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
- Programming and reasoning with algebraic effects and dependent types
This page was built for software: Idris
