The following pages link to Engineering formal metatheory (Q3189820):
Displayed 40 items.
- A Church-style intermediate language for ML\(^{\text F}\) (Q428892) (← links)
- ASP\(_{\text{fun}}\) : a typed functional active object calculus (Q433340) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
- A formalization of multi-tape Turing machines (Q744986) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- Formal metatheory of programming languages in the Matita interactive theorem prover (Q1945919) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Term-generic logic (Q2339466) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Reasoning in Abella about Structural Operational Semantics Specifications (Q2804943) (← links)
- HOCore in Coq (Q2945640) (← links)
- Disjoint Polymorphism (Q2988630) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- The Role of Indirections in Lazy Natural Semantics (Q3455082) (← links)
- Why Would You Trust B? (Q3498474) (← links)
- Nominal Inversion Principles (Q3543650) (← links)
- Formalizing Soundness of Contextual Effects (Q3543663) (← links)
- Syntax for Free: Representing Syntax with Binding Using Parametricity (Q3637185) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- (Q5111317) (← links)
- Formal SOS-Proofs for the Lambda-Calculus (Q5178966) (← links)
- A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi (Q5179010) (← links)
- Reasoning about multi-stage programs (Q5371979) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
- Psi-calculi in Isabelle (Q5895110) (← links)
- (Q6079236) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)