A correspondence between type checking via reduction and type checking via evaluation

Publication: Research - peer-reviewJournal article

  • Ilya Sergey
    Ilya Sergey
  • Dave Clark
    Dave ClarkDistriNet & IBBT, Dept. Computer Science, Katholieke Universiteit LeuvenNetherlands
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.
Original languageEnglish
JournalInformation Processing Letters
Journal publication year2012
Volume112
Journal number1-2
Pages13-20
Number of pages8
ISSN0020-0190
DOIs
StatePublished

See relations at Aarhus University Citationformats

ID: 40585470

Aarhus University
Nordre Ringgade 1
DK-8000 Aarhus C

Email: au@au.dk
Tel: +45 8715 0000
Fax: +45 8715 0201

CVR no: 31119103

AU on social media
Facebook
LinkedIn
Twitter
YouTube