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