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 Times are displayed in time zone: Tijuana, Baja California change
13:30 - 13:52 Talk | Seam: Provably Safe Local Edits on Graphs OOPSLA Manolis PapadakisStanford University, USA, Gilbert Louis BernsteinStanford University, USA, Rahul SharmaMicrosoft Research, Alex AikenStanford University, Pat HanrahanStanford University, USA DOI | ||
13:52 - 14:15 Talk | TiML: A Functional Language for Practical Complexity Analysis with Invariants OOPSLA Peng WangMassachusetts Institute of Technology, USA, Di WangPeking University, China, Adam ChlipalaMassachusetts Institute of Technology, USA DOI | ||
14:15 - 14:37 Talk | FairSquare: Probabilistic Verification of Program Fairness OOPSLA Aws AlbarghouthiUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Samuel DrewsUniversity of Wisconsin-Madison, Aditya Nori DOI | ||
14:37 - 15:00 Talk | Reasoning on Divergent Computations with Coaxioms OOPSLA DOI |