The Community for Technology Leaders
RSS Icon
Subscribe
June 24, 2008 to June 27, 2008
ISBN: 978-0-7695-3183-0
pp: 341-352
ABSTRACT
This paper presents a new bisimulation theory for parametric polymorphism which enables straight forward co-inductive proofs of program equivalences involving existential types.??The theory is an instance of typed normal form bisimulation and demonstrates the power of this recent framework for modeling typed lambda calculi as labelled transition systems.We develop our theory for a continuation-passing style calculus, Jump-With-Argument, where normal form bisimulation takes a simple form.??We equip the calculus with both existential and recursive types.??An "ultimate pattern matching theorem" enables us to define bisimilarity and we show it to be a congruence.??We apply our theory to proving program equivalences, type isomorphisms and genericity.
INDEX TERMS
typed lambda calculus, LTS, bisimulation, parametric polymorphism
CITATION
Soren B. Lassen, Paul Blain Levy, "Typed Normal Form Bisimulation for Parametric Polymorphism", LICS, 2008, Logic in Computer Science, Symposium on, Logic in Computer Science, Symposium on 2008, pp. 341-352, doi:10.1109/LICS.2008.26
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool