Mon 18 Jun 2018 11:00 - 11:30 at Columbus Ballroom B - LLVM

This talk will describe “interaction trees,” a Coq datatype for describing the behaviors of systems that interact with their environments. Several DeepSpec projects have found a use for this data structure and accompanying theory. This talk will highlight its use for defining memory models as part of the ongoing Vellvm efforts to define semantics of the LLVM IR.

Mon 18 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

11:00 - 12:15: LLVMDeepSpec at Columbus Ballroom B
11:00 - 11:30
Talk
DeepSpec
Steve ZdancewicUniversity of Pennsylvania
11:30 - 12:00
Talk
DeepSpec
Chung-Kil HurSeoul National University