swMATH20011MaRDI QIDQ31834FDOQ31834
Author name not available (Why is that?)
Official website: https://www.idris-lang.org/
Cited In (95)
- Eliminating dependent pattern matching without K
- Sequential decision problems, dependent types and generic solutions
- Unified syntax with iso-types
- The essence of ornaments
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- COCHIS: stable and coherent implicits
- Extracting functional programs from Coq, in Coq
- Elaborating dependent (co)pattern matching: no pattern left behind
- Functional modelling of musical harmony: an experience report
- The \textsc{MetaCoq} project
- 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
- Editorial: Special issue on programming with dependent types
- \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
- Incorporating quotation and evaluation into Church's type theory
- Exercising Nuprl's open-endedness
- Extracting verified decision procedures: DPLL and resolution
- Automatically proving equivalence by type-safe reflection
- Title not available (Why is that?)
- Beluga
- CLEAN
- MetaPRL
- MetaOCaml
- Agda
- Cayenne
- Cyclone
- Epigram
- AoPA
- Irdis
- FoCaLiZe
- Mtac
- Aglet
- Frank
- TCB
- MathScheme
- Lean
- CoALP
- Congruence closure in intensional type theory
- Tactics and certificates in Meta Dedukti
- Elaborator reflection: extending Idris in Idris
- 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
- 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
- Integrating induction and coinduction via closure operators and proof cycles
- Hazelnut: a bidirectionally typed structure editor calculus
- Biform theories: project description
- Theories as types
- Validating Brouwer's continuity principle for numbers using named exceptions
- MetaCoq
- finmap
- Bar induction is compatible with constructive type theory
- A verified theorem prover backend supported by a monotonic library
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- CQL
- idris-ct
- Statebox
- Guarded dependent type theory with coinductive types
- Hammer for Coq: automation for dependent type theory
- Doo bee doo bee doo
- Programming and reasoning with algebraic effects and dependent types
This page was built for software: Idris
