Pages that link to "Item:Q5747747"
From MaRDI portal
The following pages link to Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) (Q5747747):
Displaying 26 items.
- Beluga (Q14061) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Semantical analysis of contextual types (Q2200843) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Extensible Datasort Refinements (Q2988653) (← links)
- LINCX: A Linear Logical Framework with First-Class Contexts (Q2988658) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis (Q4559809) (← links)
- Plugging-in proof development environments using<i>Locks</i>in<tt>LF</tt> (Q4691186) (← links)
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- A logical framework combining model and proof theory (Q5400853) (← links)
- Finitary type theories with and without contexts (Q6053849) (← links)
- Towards substructural property-based testing (Q6102253) (← links)
- Contextual modal type theory with polymorphic contexts (Q6535241) (← links)
