Pages that link to "Item:Q5398331"
From MaRDI portal
The following pages link to Idris, a general-purpose dependently typed programming language: Design and implementation (Q5398331):
Displaying 29 items.
- Irdis (Q21669) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- Visible Type Application (Q2802481) (← links)
- Guarded Dependent Type Theory with Coinductive Types (Q2811330) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Programming up to congruence (Q2819823) (← links)
- Auto in Agda (Q2941181) (← links)
- I Got Plenty o’ Nuttin’ (Q3188289) (← links)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (Q4559809) (← links)
- Contributions to a computational theory of policy advice and avoidability (Q4577808) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- On the correctness of monadic backward induction (Q5019023) (← links)
- (Q5019311) (← links)
- Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925) (← links)
- Doo bee doo bee doo (Q5110934) (← links)
- A trustful monad for axiomatic reasoning with probability and nondeterminism (Q5152658) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
- The essence of ornaments (Q5372005) (← links)
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
- Higher-order games with dependent types (Q6049932) (← links)
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic (Q6060672) (← links)
- Adding Negation to Lambda Mu (Q6135761) (← links)
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming (Q6536347) (← links)
