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

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
VerificationOOPSLA at Regency C
Chair(s): Jonathan Edwards
13:30
22m
Talk
Seam: Provably Safe Local Edits on Graphs
OOPSLA
Manolis Papadakis Stanford University, USA, Gilbert Louis Bernstein Stanford University, USA, Rahul Sharma Microsoft Research, Alex Aiken Stanford University, Pat Hanrahan Stanford University, USA
DOI
13:52
22m
Talk
TiML: A Functional Language for Practical Complexity Analysis with Invariants
OOPSLA
Peng Wang Massachusetts Institute of Technology, USA, Di Wang Peking University, China, Adam Chlipala Massachusetts Institute of Technology, USA
DOI
14:15
22m
Talk
FairSquare: Probabilistic Verification of Program Fairness
OOPSLA
Aws Albarghouthi University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Samuel Drews University of Wisconsin-Madison, Aditya Nori
DOI
14:37
22m
Talk
Reasoning on Divergent Computations with Coaxioms
OOPSLA
Davide Ancona University of Genova, Francesco Dagnino , Elena Zucca University of Genova
DOI