coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] PiP 2017: Principles in Practice - Call for Participation

From: Peter Sewell <Peter.Sewell AT cl.cam.ac.uk>
To: types-announce AT lists.seas.upenn.edu, isabelle-users AT cl.cam.ac.uk, coq-club AT inria.fr
Subject: [Coq-Club] PiP 2017: Principles in Practice - Call for Participation
Date: Wed, 7 Dec 2016 16:54:02 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=p.m.sewell AT googlemail.com; spf=Pass smtp.mailfrom=p.m.sewell AT googlemail.com; spf=None smtp.helo=postmaster AT mail-wj0-f180.google.com
Ironport-phdr: 9a23:HeiojhLaGf0Yh8ohwtmcpTZWNBhigK39O0sv0rFitYgULfrxwZ3uMQTl6Ol3ixeRBMOAuqkC1rCd6PGoGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2timz+2pvpTVZQJVgjGwSbdzNwmt6x7cv9JQnJNvLKB3xxfU5jNJYO1cyGdsKBeOhBvm/e+7+Nho+iEWsvln6s0EGa79ZuEzSaFSJDUgKWE8osPx5iPOVQ+e2nxJamgKnwAOOAXa4RX+dpz19CDzs6x002+HPp7YV7cxDAyv86pxACTllyoDM3ZtyGzLh9Y2t69ErRaljxd7hYXdZcecP7xjffWOLpshWWNdU5MJBGR6CYSmYt5XAg==

PiP 2017: Principles in Practice

Co-located with POPL 2017

Saturday 21st January, 2017. Paris, France

Recent years have seen a number of research projects applying rigorous semantics to the analysis or design of industrially significant real-world languages and systems, in various contexts. Principles in Practice (PiP) is an informal workshop bringing together researchers to discuss the issues involved in engaging with the various industrial communities, in developing and using semantics at scale, in handling pre-existing systems complexity, and in the wide range of testing, analysis, and proof-based techniques that can be applied. There is a programme of invited talks, with no proceedings.

This follows the previous PiP 2014 workshop.

Registration

Registration is via the POPL 2017 registration page.

Preliminary Schedule

08:55 Welcome
09:00-10:00
- 09:00-09:30 Andrew Kennedy (Facebook) Static type checking for PHP
- 09:30-10:00 Jean-Louis Colaco (Ansys) Scade
10:00-10:30 coffee break
10:30-12:05 REMS session
- 10:30-10:35 Peter Sewell (Cambridge) REMS Short Introduction
- 10:35-11:05 Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project
- 11:05-11:35 Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means and why it matters
- 11:35-12:05 Philippa Gardner (Imperial) Towards Tractable Verification of _javascript_ Programs
12:05-14:00 lunch
14:00-15:30
- 14:00-14:30 John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck
- 14:30-15:00 Byron Cook (Amazon) Automated Reasoning about AWS
- 15:00-15:30 Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM
15:30-16:00 coffee break
16:00-17:30
- 16:00-16:30 Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models
- 16:30-17:30 Discussion session Methods and Tools for large-scale semantics

[Coq-Club] PiP 2017: Principles in Practice - Call for Participation, Peter Sewell, 12/07/2016