Abstractions for multi-sorted substitutions

DOI10.4230/LIPICS.ITP.2024.32MaRDI QIDQ6859995zbMATH OpenFDO

Authors Hannes Saffrich

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2024.32

zbMATH Keywords

Agdaframeworkmetatheory

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A linear algebra approach to linear metatheory
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Everybody's got to be somewhere
• scientific article; zbMATH DE number 1629944 (Why is no real title available?)
• scientific article; zbMATH DE number 177773 (Why is no real title available?)
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Nameless, painless
• Nominal unification
• Parametric higher-order abstract syntax for mechanized semantics
• POPLMark reloaded: mechanizing proofs by logical relations
• Strongly typed term representations in Coq
• The locally nameless representation
• Theorem Proving in Higher Order Logics

This page was built for publication: Abstractions for multi-sorted substitutions

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