Structured monads for generic first-order syntax metatheory

DOI10.1007/S10817-025-09731-YMaRDI QIDQ6912396zbMATH OpenFDO

Authors Lawrence Dunn, Val Tannen, Steve Zdancewic

Publication date 22 October 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-025-09731-Y

zbMATH Keywords

Coqmetatheorymonadssyntaxvariable binding

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A new approach to abstract syntax with variable binding
• A representation theorem for second-order functionals
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Applicative programming with effects
• Automated Deduction – CADE-20
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• CakeML
• Constructing Applicative Functors
• de Bruijn notation as a nested datatype
• Engineering formal metatheory
• Explicit substitutions
• First-Class Type Classes
• Free applicative functors
• GMeta: a generic formal metatheory framework for first-order representations
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Nominal logic, a first order theory of names and binding
• Ott, effective tool support for the working semanticist
• Parametric higher-order abstract syntax for mechanized semantics
• Substitution: A formal methods case study using monads and transformations
• Syntax monads for the working formal metatheorist
• Tealeaves: structured monads for generic first-order abstract syntax infrastructure
• The locally nameless representation
• Theorem Proving in Higher Order Logics
• Type classes for mathematics in type theory
• Variable binding and substitution for (nameless) dummies

This page was built for publication: Structured monads for generic first-order syntax metatheory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6912396)