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

DOI10.1145/1159803.1159826MaRDI QIDQ5501464zbMATHOpenAlexFDO

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

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)

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

Cited in

(5)

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

Describes a project that uses

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)