Pages that link to "Item:Q3183520"
From MaRDI portal
The following pages link to A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520):
Displaying 30 items.
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Flag-based big-step semantics (Q516041) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
- The effects of effects on constructivism (Q2133168) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- A relaxation of Üresin and Dubois' asynchronous fixed-point theory in Agda (Q2209538) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of universal algebra in Agda (Q2333322) (← links)
- An implementation of effective homotopy of fibrations (Q2422709) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- Exercising Nuprl’s Open-Endedness (Q2819194) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- Modular Dependent Induction in Coq, Mendler-Style (Q2829276) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language (Q2947456) (← links)
- Friends with Benefits (Q2988636) (← links)
- Bisimulations Generated from Corecursive Equations (Q3178257) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- (Q4580232) (← links)
- Normalization by Evaluation for Typed Weak lambda-Reduction (Q5091147) (← links)
- Is Impredicativity Implicitly Implicit (Q6079240) (← links)
