Hierarchical reflection

DOI10.1007/978-3-540-30142-4_5MaRDI QIDQ5464663zbMATH OpenOpenAlexFDO

Authors Luís Cruz-Filipe, Freek Wiedijk

Publication date 18 August 2005

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

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Equational reasoning via partial reflection
• Extensible and efficient automation through reflective tactics
• scientific article; zbMATH DE number 785045
• Reflection of formal tactics in a deductive reflection framework
• Types for Proofs and Programs

Cited in

(10)

• How to get more out of your oracles
• Formally proving size optimality of sorting networks
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Automatically proving equivalence by type-safe reflection
• Typing in reflective combinatory logic
• Practical reflection for sequent logics
• Compositional computational reflection
• Formalizing and proving semantic relations between specifications by reflection
• Lightweight proof by reflection using a posteriori simulation of effectful computation
• Automated Deduction – CADE-20

This page was built for publication: Hierarchical reflection

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