Modular monadic meta-theory

DOI10.1145/2500365.2500587MaRDI QIDQ5244814zbMATH OpenOpenAlexFDO

Authors Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira

Publication date 30 March 2015

Published in Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2500365.2500587

zbMATH Keywords

mechanized meta-theorymodularitymonadsside-effects

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Meta-theory à la carte
• GMeta: a generic formal metatheory framework for first-order representations
• Proof Abstraction for Imperative Languages
• Engineering formal metatheory
• Formal component-based semantics

Cited in

(11)

• Modular dependent induction in Coq, Mendler-style
• Meta-theory à la carte
• A MONADIC APPROACH TO THE MODAL THEORY
• Formal component-based semantics
• Reasoning about modular datatypes with Mendler induction
• Metric monads
• Gradual type-and-effect systems
• Proof Abstraction for Imperative Languages
• Latent Effects for Reusable Language Components
• Hefty algebras: modular elaboration of higher-order effects
• A practical formalization of monadic equational reasoning in dependent-type theory

Describes a project that uses

Uses Software

• mini-ML

This page was built for publication: Modular monadic meta-theory

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