High-level signatures and initial semantics

DOI10.4230/LIPIcs.CSL.2018.4OpenAlexW4289552732MaRDI QIDQ5079724

Ambroise Lafont, Benedikt Ahrens, Marco Maggesi, Andre Hirschowitz

Publication date: 28 May 2022

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

zbMATH Keywords

signaturessyntaxinitial semanticsmonadic substitutioncomputer-checked proofs

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (2)

Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq
• UniMath
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Substitution in non-wellfounded syntax with variable binding
• Explicit substitutions and higher-order syntax
• Modules over monads and initial semantics
• Generalised folds for nested datatypes
• Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• Second-Order Equational Logic (Extended Abstract)
• Second-Order Algebraic Theories
• Initial Algebra Semantics Is Enough!
• Modules over Monads and Linearity
• A framework for defining logics
• Proceedings 8th Workshop on Fixed Points in Computer Science
• Displayed Categories
• Monads need not be endofunctors
• Modules over relative monads for syntax and semantics

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