Idris
From MaRDI portal
Software:31834
No author found.
Related Items (39)
Automatically proving equivalence by type-safe reflection ⋮ Unnamed Item ⋮ Unified Syntax with Iso-types ⋮ I Got Plenty o’ Nuttin’ ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Hammer for Coq: automation for dependent type theory ⋮ Contributions to a computational theory of policy advice and avoidability ⋮ Extracting functional programs from Coq, in Coq ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Doo bee doo bee doo ⋮ 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 ⋮ Special issue on Programming with Dependent Types Editorial ⋮ The \textsc{MetaCoq} project ⋮ Unnamed Item ⋮ Elaborator reflection: extending Idris in Idris ⋮ Idris, a general-purpose dependently typed programming language: Design and implementation ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Functional modelling of musical harmony ⋮ Extracting verified decision procedures: DPLL and Resolution ⋮ Tactics and certificates in Meta Dedukti ⋮ Visible Type Application ⋮ Biform theories: project description ⋮ Theories as types ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ COCHIS: Stable and coherent implicits ⋮ Congruence Closure in Intensional Type Theory ⋮ Exercising Nuprl’s Open-Endedness ⋮ 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 ⋮ Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory
This page was built for software: Idris
