Pages that link to "Item:Q3183520"

The following pages link to A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520):

Displayed 40 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)
• Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) ‎ (← links)
• (Q5018487) ‎ (← links)
• Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code (Q5018778) ‎ (← links)
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi (Q5020907) ‎ (← links)
• (Q5028488) ‎ (← links)
• Characteristics of de Bruijn’s early proof checker Automath (Q5089679) ‎ (← links)
• Normalization by Evaluation for Typed Weak lambda-Reduction (Q5091147) ‎ (← links)
• How Hard Is Positive Quantification? (Q5278190) ‎ (← links)
• Containers, monads and induction recursion (Q5741557) ‎ (← links)
• A light-weight integration of automated and interactive theorem proving (Q5741559) ‎ (← links)
• On the Mints Hierarchy in First-Order Intuitionistic Logic (Q5892381) ‎ (← links)
• Formalising Mathematics in Simple Type Theory (Q6075439) ‎ (← links)