coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nikhil Swamy <nswamy AT microsoft.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] PLPV 2012: Call for participation
- Date: Fri, 2 Dec 2011 04:42:04 +0000
- Accept-language: en-US
Call for Participation
======================
PLPV 2012
The Sixth ACM SIGPLAN Workshop
Programming Languages meets Program Verification
24th January, 2012
Philadelphia, USA
(Affiliated with POPL 2012)
http://research.microsoft.com/en-us/um/people/nswamy/plpv12
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.
Registration
============
To register for PLPV 2012, please follow the instructions at:
https://regmaster3.com/2012conf/POPL12/register.php
The early registration deadline is December 24, 2011.
Hotel Information
=================
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.
Program
=======
Session 1: 9:00am-10:00am
LTL types FRP: Linear-time Temporal Logic Propositions as Types,
Proofs as Functional Reactive Programs
Alan Jeffrey
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
Vladimir Komendantsky
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
Dependent Interoperability
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
- [Coq-Club] PLPV 2012: Call for participation, Nikhil Swamy
Archive powered by MhonArc 2.6.16.