Proving Soundness of Extensional Normal-Form Bisimilarities
| Autor: | Sergueï Lenglet, Piotr Polesiuk, Dariusz Biernacki |
|---|---|
| Přispěvatelé: | Faculty of Mathematics and Computer Science [Wroclaw], University of Wrocław [Poland] (UWr), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science General Computer Science Computer science lambda calculus 0102 computer and information sciences 02 engineering and technology eta-expansion Mathematical proof 01 natural sciences Theoretical Computer Science [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Calculus Equivalence (formal languages) Equivalence (measure theory) computer.programming_language Soundness Bisimulation Computer Science - Programming Languages bisimulation up to context Proof assistant congruence 020207 software engineering control operators Extensional definition Logic in Computer Science (cs.LO) 010201 computation theory & mathematics normal-form bisimulations Computer Science::Programming Languages 020201 artificial intelligence & image processing Lambda calculus computer Programming Languages (cs.PL) |
| Zdroj: | Mathematical Foundations of Programming Semantics XXXIII Mathematical Foundations of Programming Semantics XXXIII, Jun 2017, Ljubljana, Slovenia. ⟨10.1016/j.entcs.2018.03.015⟩ Logical Methods in Computer Science Logical Methods in Computer Science, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩ MFPS Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019, 15 (1), pp.31:1-31:24. ⟨10.23638/LMCS-15(1:31)2019⟩ |
| ISSN: | 1860-5974 |
| DOI: | 10.1016/j.entcs.2018.03.015⟩ |
| Popis: | International audience; Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in lambda-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of eta-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding up to context technique are sound. We illustrate our technique with three calculi: the call-by-value lambda-calculus, the call-by-value lambda-calculus with the delimited-control operators shift and reset, and the call-by-value lambda-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the eta-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|