The following pages link to Idris (Q31834):
Displaying 39 items.
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- Biform theories: project description (Q1798949) (← links)
- Theories as types (Q1799118) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches (Q2335952) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- Visible Type Application (Q2802481) (← links)
- Guarded Dependent Type Theory with Coinductive Types (Q2811330) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
- (Q2980971) (← links)
- Elaborator reflection: extending Idris in Idris (Q2985777) (← links)
- Unified Syntax with Iso-types (Q3179296) (← links)
- I Got Plenty o’ Nuttin’ (Q3188289) (← links)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (Q4559809) (← links)
- Contributions to a computational theory of policy advice and avoidability (Q4577808) (← links)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
- COCHIS: Stable and coherent implicits (Q4972074) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- (Q5019311) (← links)
- Extracting functional programs from Coq, in Coq (Q5101927) (← links)
- Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925) (← links)
- Doo bee doo bee doo (Q5110934) (← links)
- A trustful monad for axiomatic reasoning with probability and nondeterminism (Q5152658) (← links)
- Functional modelling of musical harmony (Q5176972) (← links)
- Extracting verified decision procedures: DPLL and Resolution (Q5177337) (← links)
- A Verified Theorem Prover Backend Supported by a Monotonic Library (Q5222980) (← links)
- Bar Induction is Compatible with Constructive Type Theory (Q5244386) (← links)
- Programming and reasoning with algebraic effects and dependent types (Q5244796) (← links)
- Hazelnut: a bidirectionally typed structure editor calculus (Q5370848) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
- The essence of ornaments (Q5372005) (← links)
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
- Special issue on Programming with Dependent Types Editorial (Q5372011) (← links)
- Idris, a general-purpose dependently typed programming language: Design and implementation (Q5398331) (← links)
