Abstract
The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets interpreted in the domain of discourse. By allowing the interpretation function to be partial or even a relation one gets a more general method known as "partial reflection". In this paper we show how one can take advantage of the partiality of the interpretation to uniformly define a family of tactics for equational reasoning that will work in different algebraic structures. The tactics then follow the hierarchy of those algebraic structures in a natural way. © Springer-Verlag 2004.
Cite
CITATION STYLE
Cruz-Filipe, L., & Wiedijk, F. (2004). Hierarchical Reflection. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3223, 66–81. https://doi.org/10.1007/978-3-540-30142-4_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
