[TYPES/announce] PLPV 2012: Call for participation
nswamy at microsoft.com
Thu Dec 1 23:41:19 EST 2011
Call for Participation
The Sixth ACM SIGPLAN Workshop
Programming Languages meets Program Verification
24th January, 2012
(Affiliated with POPL 2012)
You are cordially invited to PLPV 2012.
The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification, by
bringing together experts from diverse areas like types, contracts,
interactive theorem proving, model checking and program analysis. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic or structural
properties of the programming language. Examples include dependently
typed programming languages, which leverage a language's type system
to specify and check richer than usual specifications or extended
static checking systems which incorporate contracts with either static
or dynamic contract checking.
To register for PLPV 2012, please follow the instructions at:
The early registration deadline is December 24, 2011.
PLPV will be co-located with POPL at the Sheraton Society Hill Hotel
in Philadelphia. Please visit POPL's web site to make reservations at
the special conference rate.
Session 1: 9:00am-10:00am
LTL types FRP: Linear-time Temporal Logic Propositions as Types,
Proofs as Functional Reactive Programs
A Hoare Calculus for the Verification of Synchronous Languages
Manuel Gesell and Klaus Schneider
Session 2: 10:30am-12:00pm
Invited talk: Could We Verify an Information-flow Computer?
Benjamin C. Pierce
University of Pennsylvania
Lunch: 12:00pm-2:00pm (not provided)
Session 3: 2:00pm-3:30pm
Reflexive Toolbox for Regular Expression Matching
Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work
Reynald Affeldt, David Nowak and Yutaka Oiwa
The VerCors project - setting up basecamp
Afshin Amighi, Stefan Blom, Marieke Huisman and Marina Zaharieva-Stojanovski
Session 4: 4:00pm-5:00pm
Peter-Michael Osera, Vilhelm Sjoberg and Steve Zdancewic.
Equational Reasoning about Programs with General Recursion and Call-by-value Semantics
Garrin Kimmell, Aaron Stump, Harley Eades, Peng Fu, Tim Sheard, Stephanie Weirich,
Chris Casinghino, Vilhelm Sjoberg, Nathan Collins and Ki Yung Ahn
More information about the Types-announce