The following pages link to Irdis (Q21669):
Displaying 22 items.
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← 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)
- Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
- Unified Syntax with Iso-types (Q3179296) (← 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)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← 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)
- 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)
- Combining proofs and programs in a dependently typed language (Q5408400) (← links)
