TY - GEN
T1 - Abstract interpretation of annotated commands
AU - Nipkow, Tobias
PY - 2012
Y1 - 2012
N2 - This paper formalizes a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalization, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.
AB - This paper formalizes a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalization, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.
UR - http://www.scopus.com/inward/record.url?scp=84865606343&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-32347-8_9
DO - 10.1007/978-3-642-32347-8_9
M3 - Conference contribution
AN - SCOPUS:84865606343
SN - 9783642323461
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 116
EP - 132
BT - Interactive Theorem Proving - Third International Conference, ITP 2012, Proceedings
T2 - 3rd International Conference on Interactive Theorem Proving, ITP 2012
Y2 - 13 August 2012 through 15 August 2012
ER -