Engineering formal metatheory
From MaRDI portal
Publication:3189820
DOI10.1145/1328438.1328443zbMath1295.68052OpenAlexW2025431400MaRDI QIDQ3189820
Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich
Publication date: 12 September 2014
Published in: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1394&context=cis_papers
Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal metatheory of the lambda calculus using Stoughton's substitution, The Role of Indirections in Lazy Natural Semantics, A canonical locally named representation of binding, A two-level logic approach to reasoning about computations, HOCore in Coq, Why Would You Trust B?, A formalized general theory of syntax with bindings, Rensets and renaming-based recursion for syntax with bindings extended version, Mechanizing type environments in weak HOAS, 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 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, Reasoning about multi-stage programs, Unnamed Item, Psi-calculi in Isabelle, Psi-calculi in Isabelle, Disjoint Polymorphism, Nominal techniques in Isabelle/HOL, Nominal Inversion Principles, Formalizing Soundness of Contextual Effects, A formalized general theory of syntax with bindings: extended version, Alpha-structural induction and recursion for the lambda calculus in constructive type theory, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, External and internal syntax of the \(\lambda \)-calculus, Formal SOS-Proofs for the Lambda-Calculus, A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, Reasoning in Abella about Structural Operational Semantics Specifications, Unnamed Item, Viewing \({\lambda}\)-terms through maps, A formalization of multi-tape Turing machines, The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus, Syntax for Free: Representing Syntax with Binding Using Parametricity, Mechanizing the Metatheory of mini-XQuery, Mechanized metatheory revisited, Term-generic logic, Mechanizing metatheory without typing contexts
Uses Software
