Engineering formal metatheory
From MaRDI portal
Recommendations
Cited in
(60)- A formalized general theory of syntax with bindings
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- The locally nameless representation
- A solution to the PoplMark challenge based on de Bruijn indices
- Nested abstract syntax in Coq
- Formal metatheory of programming languages in the Matita interactive theorem prover
- A list-machine benchmark for mechanized metatheory
- A formalized general theory of syntax with bindings: extended version
- Mechanized metatheory revisited
- Term-generic logic
- Mechanizing metatheory without typing contexts
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Strongly typed term representations in Coq
- A canonical locally named representation of binding
- A two-level logic approach to reasoning about computations
- Reasoning in Abella about structural operational semantics specifications
- GMeta: a generic formal metatheory framework for first-order representations
- Meta-theory à la carte
- HOCore in Coq
- Disjoint polymorphism
- Mechanizing the metatheory of mini-XQuery
- Towards a mechanized metatheory of Standard ML
- The role of indirections in lazy natural semantics
- Why Would You Trust B?
- Nominal Inversion Principles
- Formalizing Soundness of Contextual Effects
- Barendregt’s Variable Convention in Rule Inductions
- Syntax for Free: Representing Syntax with Binding Using Parametricity
- Abstract metaprolog engine
- A Church-style intermediate language for ML\(^{\text F}\)
- ASP\(_{\text{fun}}\) : a typed functional active object calculus
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Formalizing the meta-theory of first-order predicate logic
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Formal SOS-Proofs for the Lambda-Calculus
- A flexible framework for visualisation of computational properties of general explicit substitutions calculi
- Modular monadic meta-theory
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- Handcrafted inversions made operational on operational semantics
- Reasoning about multi-stage programs
- Typed Lambda Calculi and Applications
- Psi-calculi in Isabelle
- Psi-calculi in Isabelle
- Types for Proofs and Programs
- \(\eta\)-equivalence in core dependent Haskell
- Rensets and renaming-based recursion for syntax with bindings extended version
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Structured monads for generic first-order syntax metatheory
- Pure type systems without explicit contexts
- A simple blame calculus for explicit nulls
- Recursive subtyping for all
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
- Mechanising Böhm trees and -completeness
- Viewing \({\lambda}\)-terms through maps
- A formalization of multi-tape Turing machines
- Mechanizing type environments in weak HOAS
- Nominal techniques in Isabelle/HOL
- External and internal syntax of the \(\lambda \)-calculus
This page was built for publication: Engineering formal metatheory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3189820)
