A logic for parametric polymorphism with effects

Alexander Simpson, Rasmus Mogelberg

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)


We present a logic for reasoning about parametric polymorphism in combination with arbitrary computational effects (nondeterminism, exceptions, continuations, side-effects etc.). As examples of reasoning in the logic, we show how to verify correctness of polymorphic type encodings in the presence of effects.
Original languageEnglish
Title of host publicationTypes for Proofs and Programs
Subtitle of host publicationInternational Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007 Revised Selected Papers
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-68103-8
ISBN (Print)978-3-540-68084-0
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'A logic for parametric polymorphism with effects'. Together they form a unique fingerprint.

Cite this