Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection

DOI10.1145/1159803.1159826zbMATH Open1321.68194OpenAlexW2081798440MaRDI QIDQ5501464FDOQ5501464

Authors:

Publication date: 3 August 2015

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

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

Recommendations

• GMeta: a generic formal metatheory framework for first-order representations
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• Reasoning with higher-order abstract syntax in a logical framework
• Mechanizing metatheory in a logical framework
• Mechanized metatheory revisited

zbMATH Keywords

reflectiontype theoryhigher-order abstract syntaxmechanized reasoningMetaPRLmeta-theorylanguages with bindingsNuPRL

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (5)

• Mechanized metatheory revisited
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Meta-programming with built-in type equality
• Practical reflection for sequent logics
• GMeta: a generic formal metatheory framework for first-order representations

Uses Software

• MetaPRL
• Nuprl

This page was built for publication: Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection

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