Irdis

swMATH9690MaRDI QIDQ21669FDOQ21669

Author name not available (Why is that?)

Described by source

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

Cited In (22)

• Eliminating dependent pattern matching without K
• I got plenty o' nuttin'
• Proof-relevant Horn clauses for dependent type inference and term synthesis
• \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
• Exercising Nuprl's open-endedness
• Unified syntax with iso-types
• Automatically proving equivalence by type-safe reflection
• The essence of ornaments
• Title not available (Why is that?)
• Type-specialized staged programming with process separation
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Congruence closure in intensional type theory
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• Integrating induction and coinduction via closure operators and proof cycles
• Validating Brouwer's continuity principle for numbers using named exceptions
• 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
• Combining proofs and programs in a dependently typed language

This page was built for software: Irdis