Idris

swMATH20011MaRDI QIDQ31834FDOQ31834

Author name not available (Why is that?)

Cited In (39)

• Eliminating dependent pattern matching without K
• Extracting verified decision procedures: DPLL and Resolution
• Guarded Dependent Type Theory with Coinductive Types
• The \textsc{MetaCoq} project
• Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches
• COCHIS: Stable and coherent implicits
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Contributions to a computational theory of policy advice and avoidability
• Exercising Nuprl’s Open-Endedness
• Incorporating quotation and evaluation into Church's type theory
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Bar Induction is Compatible with Constructive Type Theory
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• I Got Plenty o’ Nuttin’
• Automatically proving equivalence by type-safe reflection
• Visible Type Application
• The essence of ornaments
• Elaborating dependent (co)pattern matching: No pattern left behind
• Title not available (Why is that?)
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Tactics and certificates in Meta Dedukti
• Elaborator reflection: extending Idris in Idris
• 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
• Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
• 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
• Extracting functional programs from Coq, in Coq
• Unified Syntax with Iso-types
• Functional modelling of musical harmony
• Congruence Closure in Intensional Type Theory
• Special issue on Programming with Dependent Types Editorial
• Hammer for Coq: automation for dependent type theory
• Doo bee doo bee doo
• Programming and reasoning with algebraic effects and dependent types
• Title not available (Why is that?)

This page was built for software: Idris