Title: A correspondence between type checking via reduction and type checking via evaluation
Authors: Sergey, Ilya ×
Clarke, Dave #
Issue Date: 15-Jan-2012
Series Title: Information Processing Letters vol:112 issue:1-2 pages:13-20
Abstract: We describe a derivational approach to proving the equivalence of different representations of a type system. Different ways of representing type assignments are convenient for particular applications such as reasoning or implementation, but some kind of correspondence between them should be proven. In this paper we address two such semantics for type checking: one, due to Kuan et al., in the form of a term rewriting system and the other in the form of a traditional set of derivation rules. By employing a set of techniques investigated by Danvy et al., we mechanically derive the correspondence between a reduction-based semantics for type-checking and a traditional one in the form of derivation rules, implemented as a recursive descent. The correspondence is established through a series of semantics-preserving functional program transformations.
ISSN: 0020-0190
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
sergey-ipl11.pdfsubmitted article Published 159KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science