Irdis

swMATH9690MaRDI QIDQ21669

No author found.

Described by source

• Idris, a general-purpose dependently typed programming language: Design and implementation

Related Items (22)

Automatically proving equivalence by type-safe reflection ⋮ 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 ⋮ Type-specialized staged programming with process separation ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Doo bee doo bee doo ⋮ Eliminating dependent pattern matching without K ⋮ The essence of ornaments ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Unnamed Item ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Combining proofs and programs in a dependently typed language ⋮ Visible Type Application ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Congruence Closure in Intensional Type Theory ⋮ Exercising Nuprl’s Open-Endedness ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

This page was built for software: Irdis