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 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | 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 22mTalk | 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 22mTalk | 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 22mTalk | Reasoning on Divergent Computations with Coaxioms OOPSLA DOI |