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

DOI10.1145/1159803.1159826zbMath1321.68194OpenAlexW2081798440MaRDI QIDQ5501464

No author found.

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)

Related Items (1)

Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax

Uses Software

• MetaPRL
• Nuprl

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