DROPS

Artifact

Software

T-Rex

Authors: Raphael Douglas Giles and Vincent Jackson

Abstract

Cite as

Raphael Douglas Giles, Vincent Jackson. T-Rex (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22483,
   title = {{T-Rex}}, 
   author = {Douglas Giles, Raphael and Jackson, Vincent},
   note = {Software, version 1.0.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:c7dd8ada9bdd696f86cd11bc6751817ed37ad120;origin=https://github.com/vjackson725/term_check;visit=swh:1:snp:07ec14cdddac6edf61e39a952fb12b8ead2016a7;anchor=swh:1:rev:febbde1e4ad3af86aa44f97ce5cabcde2e23f594}{\texttt{swh:1:dir:c7dd8ada9bdd696f86cd11bc6751817ed37ad120}} (visited on 2024-11-28)},
   url = {https://github.com/vjackson725/term_check},
   doi = {10.4230/artifacts.22483},
}

Artifact

Software

DOI: 10.4230/artifacts.22484

Abstract

Cite as

Vincent Jackson. General RGSep (Software, Mechanised Proof). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22484,
   title = {{General RGSep}}, 
   author = {Jackson, Vincent},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:e759950d2ebd7571c86913f8296dfb29aa24a108;origin=https://github.com/vjackson725/GeneralRGSep;visit=swh:1:snp:e72ee116f86e47757d405779e79638178e413d3a;anchor=swh:1:rev:f35714d61e01b378ec363cc3f5fd6f5965a54beb}{\texttt{swh:1:dir:e759950d2ebd7571c86913f8296dfb29aa24a108}} (visited on 2024-11-28)},
   url = {https://github.com/vjackson725/GeneralRGSep/tree/itp24},
   doi = {10.4230/artifacts.22484},
}

Document

DOI: 10.4230/LIPIcs.ITP.2024.23

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Authors: Vincent Jackson, Toby Murray, and Christine Rizkallah

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

This paper describes GenRGSep, an Isabelle/HOL library for the development of RGSep logics using a general algebraic state model. In particular, we develop an algebraic state models based on resource algebras that assume neither the presence of unit resources or the cancellativity law. If a new resource model is required, its components need only be proven an instance of a permission algebra, and then they can be composed together using tuples and functions. The proof of soundness is performed by Vafeiadis' operational soundness method. This method was originally formulated with respect to a concrete heap model. This paper adapts it to account for the absence of both units as well as the cancellativity law.

Cite as

Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
  author =	{Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
  title =	{{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
  URN =		{urn:nbn:de:0030-drops-207510},
  doi =		{10.4230/LIPIcs.ITP.2024.23},
  annote =	{Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2024.139

T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations

Authors: Raphael Douglas Giles, Vincent Jackson, and Christine Rizkallah

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract

We introduce a powerful termination algorithm for structurally recursive functions that improves on the core ideas behind lexicographic termination algorithms for functional programs. The algorithm generates linear-lexicographic combinations of primitive measure functions measuring the recursive structure of terms. We introduce a measure language that enables the simplification and comparison of measures and we prove meta-theoretic properties of our measure language. Moreover, we demonstrate our algorithm, on an untyped first-order functional language and prove its soundness and that it runs in polynomial time. We also provide a Haskell implementation. As part of this work, we also show how to solve the maximisation of negative vector-components as a linear program.

Cite as

Raphael Douglas Giles, Vincent Jackson, and Christine Rizkallah. T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 139:1-139:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{giles_et_al:LIPIcs.ICALP.2024.139,
  author =	{Giles, Raphael Douglas and Jackson, Vincent and Rizkallah, Christine},
  title =	{{T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{139:1--139:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.139},
  URN =		{urn:nbn:de:0030-drops-202827},
  doi =		{10.4230/LIPIcs.ICALP.2024.139},
  annote =	{Keywords: Termination, Recursive functions}
}

Search Results

Documents authored by Jackson, Vincent

T-Rex

Abstract

Cite as

General RGSep

Abstract

Cite as

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras

Abstract

Cite as

T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations

Abstract

Cite as

Thanks for your feedback!

Could not send message