scientific article; zbMATH DE number 7379288

DOI10.23638/LMCS-17(2:17)2021MaRDI QIDQ5009703

Benedikt Ahrens, Ambroise Lafont, Marco Maggesi, Andre Hirschowitz

Publication date: 5 August 2021

Full work available at URL: https://arxiv.org/abs/1805.03740

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

signaturesyntaxinitial semanticscomputer-checked proofmonadic substitution

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (1)

Variable binding and substitution for (nameless) dummies

Uses Software

• Coq
• UniMath
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• On the construction of free algebras for equational systems
• Substitution: A formal methods case study using monads and transformations
• The differential lambda-calculus
• On tree coalgebras and coalgebra presentations
• Generalised folds for nested datatypes
• A fixpoint theorem for complete categories
• Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
• The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads
• Displayed Categories
• Tensor categorical foundations of algebraic geometry
• 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
• Explicit substitutions
• Monads need not be endofunctors
• Initial Semantics for higher-order typed syntax in Coq
• Univalent categories and the Rezk completion
• Modules over relative monads for syntax and semantics

This page was built for publication: