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: (GMT-04:00) Eastern Time (US & Canada) change

11:00 - 12:15: DeepSpec 2018 - LLVM at Columbus Ballroom B
deepspec-2018-papers11:00 - 11:30
Steve ZdancewicUniversity of Pennsylvania
deepspec-2018-papers11:30 - 12:00
Chung-Kil HurSeoul National University