PLDI 2019 (series) / DeepSpec 2019 (series) /
DeepSpec 2019 Program
This is the DeepSpec 2019 program - see the full program for PLDI 2019 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 22 JunDisplayed time zone: Tijuana, Baja California change
Sat 22 Jun
Displayed time zone: Tijuana, Baja California change
09:00 - 10:30 | |||
09:00 45mTalk | Overview of the DeepSpec Expedition and its Capstone Application DeepSpec Benjamin C. Pierce University of Pennsylvania | ||
09:45 45mTalk | Project Updates from Participating Sites DeepSpec Andrew W. Appel Princeton, Adam Chlipala Massachusetts Institute of Technology, USA, Zhong Shao Yale University |
11:00 - 12:30 | |||
11:00 30mTalk | Closure Conversion is Safe for Space DeepSpec | ||
11:30 30mTalk | Fast, Verified Partial Evaluation DeepSpec Adam Chlipala Massachusetts Institute of Technology, USA | ||
12:00 30mTalk | Stack-Aware CompCert DeepSpec Yuting Wang Yale University |
14:00 - 15:30 | |||
14:00 30mTalk | Abstraction, Subsumption, and Linking in VST DeepSpec | ||
14:30 30mTalk | Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation DeepSpec Mengqi Liu Yale University | ||
15:00 30mTalk | Modular Correctness Proofs at the Hardware-Software Interface DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA |
16:00 - 17:30 | |||
16:00 20mTalk | Interaction Trees: Representing Recursive and Impure Programs in Coq DeepSpec Steve Zdancewic University of Pennsylvania | ||
16:20 25mTalk | Connecting Separation Logic with First-Order Reasoning on Memory DeepSpec | ||
16:45 45mTalk | Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control) DeepSpec Daan Leijen Microsoft Research, USA |
Sun 23 JunDisplayed time zone: Tijuana, Baja California change
Sun 23 Jun
Displayed time zone: Tijuana, Baja California change
09:00 - 10:30 | Interaction Trees and Algebraic Effects IIDeepSpec at 106B Chair(s): Steve Zdancewic University of Pennsylvania | ||
09:00 45mTalk | Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec DeepSpec Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2 | ||
09:45 45mTalk | Names, Places, and Things: Generic Traversals over Generic Syntax with Binding DeepSpec James McKinna University of Edinburgh |
11:00 - 12:30 | HW/SW Interface SpecificationsDeepSpec at 106B Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA | ||
11:00 45mTalk | Development of the RISC-V ISA Formal Specification DeepSpec | ||
11:45 45mTalk | Automated Formal Memory Consistency Verification of Hardware DeepSpec Yatin Manerkar Princeton University |
14:00 - 15:15 | |||
14:00 45mTalk | Project Oak: Control Data in Distributed Systems, Verify All The Things DeepSpec Ben Laurie Google Research | ||
14:45 30mTalk | Refinement-Based Game Semantics for CompCert DeepSpec Jérémie Koenig Yale University |
15:45 - 16:45 | |||
15:45 30mTalk | Coinductive Reasoning about Interaction Trees DeepSpec Chung-Kil Hur Seoul National University | ||
16:15 30mTalk | Coverage Guided, Property Based Testing DeepSpec Leonidas Lampropoulos University of Pennsylvania |