2 Search Results for "Weber, Tjark"

Document
DOI: 10.4230/LIPIcs.ITP.2022.15
A Verified Cyclicity Checker: For Theories with Overloaded Constants

Authors: Arve Gengelbach and Johannes Åman Pohjola

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.
Cite as

Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15,
  author =	{Gengelbach, Arve and \r{A}man Pohjola, Johannes},
  title =	{{A Verified Cyclicity Checker: For Theories with Overloaded Constants}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15},
  URN =		{urn:nbn:de:0030-drops-167240},
  doi =		{10.4230/LIPIcs.ITP.2022.15},
  annote =	{Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.198
Modal Logics for Nominal Transition Systems

Authors: Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.
Cite as

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 198-211, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{parrow_et_al:LIPIcs.CONCUR.2015.198,
  author =	{Parrow, Joachim and Borgstr\"{o}m, Johannes and Eriksson, Lars-Henrik and Gutkovas, Ramunas and Weber, Tjark},
  title =	{{Modal Logics for Nominal Transition Systems}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{198--211},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.198},
  URN =		{urn:nbn:de:0030-drops-53823},
  doi =		{10.4230/LIPIcs.CONCUR.2015.198},
  annote =	{Keywords: Process algebra, nominal sets, bisimulation, modal logic}
}
  • Refine by Author
  • 1 Borgström, Johannes
  • 1 Eriksson, Lars-Henrik
  • 1 Gengelbach, Arve
  • 1 Gutkovas, Ramunas
  • 1 Parrow, Joachim
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Correctness
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Isabelle/HOL
  • 1 Process algebra
  • 1 ad-hoc overloading
  • 1 bisimulation
  • 1 cyclicity
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact