High-level signatures and initial semantics

DOI10.4230/LIPICS.CSL.2018.4MaRDI QIDQ5079724zbMATH OpenOpenAlexFDO

Authors Benedikt Ahrens, Ambroise Lafont, Marco Maggesi, André Hirschowitz

Publication date 28 May 2022

Full work available at URL https://inria.hal.science/hal-01930058

zbMATH Keywords

computer-checked proofsinitial semanticsmonadic substitutionsignaturessyntax

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 7379288
• From signatures to monads in \textsf{UniMath}
• Initiality for typed syntax and semantics
• Initiality for typed syntax and semantics
• Initial semantics for strengthened signatures

Cites work

• A framework for defining logics
• Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
• Displayed Categories
• Explicit substitutions and higher-order syntax
• Generalised folds for nested datatypes
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 977284 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• Initial Algebra Semantics Is Enough!
• Linear logic
• Modules over monads and initial semantics
• Modules over Monads and Linearity
• Modules over relative monads for syntax and semantics
• Monads need not be endofunctors
• Proceedings of the 8th workshop on fixed points in computer science, Tallinn, Estonia, March 24, 2012
• Second-Order Algebraic Theories
• Second-Order Equational Logic (Extended Abstract)
• Substitution in non-wellfounded syntax with variable binding
• The category theoretic understanding of universal algebra: Lawvere theories and monads

Cited in

(5)

• scientific article; zbMATH DE number 7379288 (Why is no real title available?)
• Modular specification of monads through higher-order presentations
• Modules over monads and operational semantics (expanded version)
• Universal algebra in UniMath
• Scott's representation theorem and the univalent Karoubi envelope

Describes a project that uses

Uses Software

• UniMath
• Coq
• GitHub

This page was built for publication: High-level signatures and initial semantics

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