Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 14:37 - 15:00 at Regency C - Verification Chair(s): Jonathan Edwards

Coaxioms have been recently introduced to enhance the expressive power of inference systems, by supporting interpretations which are neither purely inductive, nor coinductive. This paper proposes a novel approach based on coaxioms to capture divergence in semantic definitions by allowing inductive and coinductive semantic rules to be merged together for defining a unique semantic judgment. In particular, coinduction is used to derive a special result which models divergence. In this way, divergent, terminating, and stuck computations can be properly distinguished even in semantic definitions where this is typically difficult, as in big-step style. We show how the proposed approach can be applied to several languages; in particular, we first illustrate it on the paradigmatic example of the λ-calculus, then show how it can be adopted for defining the big-step semantics of a simple imperative Java-like language. We provide proof techniques to show classical results, including equivalence with small-step semantics, and type soundness for typed versions of both languages.

Thu 26 Oct

splash-2017-OOPSLA
13:30 - 15:00: OOPSLA - Verification at Regency C
Chair(s): Jonathan Edwards
splash-2017-OOPSLA150901740000013:30 - 13:52
Talk
Manolis PapadakisStanford University, USA, Gilbert Louis BernsteinStanford University, USA, Rahul SharmaMicrosoft Research, Alex AikenStanford University, Pat HanrahanStanford University, USA
DOI
splash-2017-OOPSLA150901875000013:52 - 14:15
Talk
Peng WangMassachusetts Institute of Technology, USA, Di WangPeking University, China, Adam ChlipalaMassachusetts Institute of Technology, USA
DOI
splash-2017-OOPSLA150902010000014:15 - 14:37
Talk
Aws AlbarghouthiUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Samuel DrewsUniversity of Wisconsin-Madison, Aditya Nori
DOI
splash-2017-OOPSLA150902145000014:37 - 15:00
Talk
Davide AnconaUniversity of Genova, Francesco Dagnino, Elena ZuccaUniversity of Genova
DOI