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

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