Multi-level meta-reasoning with higher-order abstract syntax

DOI10.1007/3-540-36576-1_24MaRDI QIDQ4417871zbMATH OpenFDO

Authors Alberto Momigliano, Simon J. Ambler

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2620/26200375.htm

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Combining higher order abstract syntax with tactical theorem proving and (co)induction
• Reasoning with higher-order abstract syntax in a logical framework
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Two-level meta-reasoning in Coq

Cited in

(9)

• Cut elimination for a logic with induction and co-induction
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Abstract metaprolog engine
• Automated reasoning with a constraint-based metainterpreter
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Combining higher order abstract syntax with tactical theorem proving and (co)induction
• Two-level meta-reasoning in Coq
• Reasoning with higher-order abstract syntax in a logical framework

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle
• mini-ML

This page was built for publication: Multi-level meta-reasoning with higher-order abstract syntax

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