Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 10:30 - 10:52 at Aurora Borealis - Program Verification Chair(s): Adam Chlipala

Rasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

Wed 21 Aug

icfp-2019-papers
10:30 - 12:00: Research Papers - Program Verification at Aurora Borealis
Chair(s): Adam ChlipalaMassachusetts Institute of Technology
icfp-2019-papers10:30 - 10:52
Talk
Wouter SwierstraUtrecht University, Netherlands, Tim BaanenUtrecht University
icfp-2019-papers10:52 - 11:15
Talk
Kenji MaillardInria Paris and ENS Paris, Danel AhmanUniversity of Ljubljana, Robert AtkeyUniversity of Strathclyde, Guido MartínezCIFASIS-CONICET, Argentina, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Éric TanterUniversity of Chile & Inria Paris
Pre-print
icfp-2019-papers11:15 - 11:37
Talk
Amin Timanyimec-Distrinet KU-Leuven, Lars BirkedalAarhus University
icfp-2019-papers11:37 - 12:00
Talk
Nicholas V. LewchenkoUniversity of Colorado Boulder, Arjun RadhakrishnaMicrosoft, Akash Gaonkar, Pavol CernyUniversity of Colorado Boulder
DOI Pre-print