Idris

swMATH20011MaRDI QIDQ31834FDOQ31834

Author name not available (Why is that?)

Cited In (39)

• Eliminating dependent pattern matching without K
• 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
• Sequential decision problems, dependent types and generic solutions
• Extracting verified decision procedures: DPLL and resolution
• Unified syntax with iso-types
• Automatically proving equivalence by type-safe reflection
• The essence of ornaments
• Title not available (Why is that?)
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Congruence closure in intensional type theory
• Tactics and certificates in Meta Dedukti
• COCHIS: stable and coherent implicits
• 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
• 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
• Bar induction is compatible with constructive type theory
• Extracting functional programs from Coq, in Coq
• A verified theorem prover backend supported by a monotonic library
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Guarded dependent type theory with coinductive types
• Elaborating dependent (co)pattern matching: no pattern left behind
• 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