VenuePhoenix Convention Center
Room name106B
Floor0
Room number106B
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sat 22 Jun
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:30
Deep SpecificationsDeepSpec at 106B
Chair(s): Lennart BeringerPrinceton University
09:00
45m
Talk
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Benjamin C. PierceUniversity of Pennsylvania
09:45
45m
Talk
Project Updates from Participating Sites
DeepSpec
Andrew AppelPrinceton, Adam ChlipalaMassachusetts Institute of Technology, USA, Zhong ShaoYale University
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
Compiler VerificationDeepSpec at 106B
Chair(s): Zhong ShaoYale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting WangYale University
14:00 - 15:30
Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart BeringerPrinceton University, Andrew AppelPrinceton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi LiuYale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon ChoiMassachusetts Institute of Technology, USA
16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew AppelPrinceton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve ZdancewicUniversity of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William ManskyUniversity of Illinois at Chicago, Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan LeijenMicrosoft Research, USA

Sun 23 Jun
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:30
Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve ZdancewicUniversity of Pennsylvania
09:00
45m
Talk
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
09:45
45m
Talk
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
DeepSpec
James McKinnaUniversity of Edinburgh
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
HW/SW Interface SpecificationsDeepSpec at 106B
Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA
11:00
45m
Talk
Development of the RISC-V ISA Formal Specification
DeepSpec
11:45
45m
Talk
Automated Formal Memory Consistency Verification of Hardware
DeepSpec
Yatin ManerkarPrinceton University
14:00 - 15:15
Verifying All the ThingsDeepSpec at 106B
Chair(s): Zhong ShaoYale University
14:00
45m
Talk
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Ben LaurieGoogle Research
14:45
30m
Talk
Refinement-Based Game Semantics for CompCert
DeepSpec
Jérémie KoenigYale University
15:15 - 15:45
Coffee BreakDeepSpec at 106B
15:45 - 16:45
Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart BeringerPrinceton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil HurSeoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas LampropoulosUniversity of Pennsylvania

Sat 22 Jun
Times are displayed in time zone: Tijuana, Baja California change