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
• Guarded Dependent Type Theory with Coinductive Types
• \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
• 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?)
• Type-specialized staged programming with process separation
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
• Integrating induction and coinduction via closure operators and proof cycles
• Validating Brouwer's continuity principle for numbers using named exceptions
• Unified Syntax with Iso-types
• Congruence Closure in Intensional Type Theory
• 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