CycleQ: An Efficient Basis for Cyclic Equational Reasoning

Eddie C Jones; Luke Ong; Steven Ramsay

doi:10.1145/3519939.3523731

CycleQ: An Efficient Basis for Cyclic Equational Reasoning

Eddie C Jones, Luke Ong, Steven Ramsay

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

4 Citations (Scopus)

103 Downloads (Pure)

Abstract

We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proofs and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, implemented as a GHC plugin, shows promising results on a number of standard benchmarks.

Original language	English
Title of host publication	PLDI 2022
Subtitle of host publication	Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Editors	Ranjit Jhala, Isil Dillig
Publisher	Association for Computing Machinery (ACM)
Pages	395-409
Number of pages	15
ISBN (Electronic)	9781450392655
DOIs	https://doi.org/10.1145/3519939.3523731
Publication status	Published - 9 Jun 2022
Event	The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation - The Catamaran Resort, 3999 Mission Boulevard, 92109, San Diego, California , United States Duration: 13 Jun 2022 → 17 Jun 2022 https://pldi22.sigplan.org/

Publication series

Name	Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
ISSN (Electronic)	1531-7102

Conference

Conference	The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation
Abbreviated title	PLDI 2022
Country/Territory	United States
City	San Diego, California
Period	13/06/22 → 17/06/22
Internet address	https://pldi22.sigplan.org/

Bibliographical note

Funding Information:
We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006579/1, EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems.

Publisher Copyright:
© 2022 ACM.

Research Groups and Themes

Programming Languages

Keywords

Theory of computation
Equational logic and rewriting
Logic and verification.

Access to Document

10.1145/3519939.3523731Licence: Other

Full-text PDF (accepted author manuscript)
This is the accepted author manuscript (AAM). The final published version (version of record) is available online via ACM at https://doi.org/10.1145/3519939.3523731. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 687 KB

Handle.net

Persistent link

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses
Ramsay, S. (Principal Investigator)
1/03/20 → 28/02/23
Project: Research

Cite this

Jones, E. C., Ong, L., & Ramsay, S. (2022). CycleQ: An Efficient Basis for Cyclic Equational Reasoning. In R. Jhala, & I. Dillig (Eds.), PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 395-409). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery (ACM). https://doi.org/10.1145/3519939.3523731

Jones, Eddie C ; Ong, Luke ; Ramsay, Steven. / CycleQ : An Efficient Basis for Cyclic Equational Reasoning. PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. editor / Ranjit Jhala ; Isil Dillig. Association for Computing Machinery (ACM), 2022. pp. 395-409 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

@inproceedings{427ccfbc5dc64de69e474c1ba2dac2ab,

title = "CycleQ: An Efficient Basis for Cyclic Equational Reasoning",

abstract = "We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proofs and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, implemented as a GHC plugin, shows promising results on a number of standard benchmarks.",

keywords = "Theory of computation, Equational logic and rewriting, Logic and verification.",

author = "Jones, {Eddie C} and Luke Ong and Steven Ramsay",

note = "Funding Information: We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006579/1, EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems. Publisher Copyright: {\textcopyright} 2022 ACM.; The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2022 ; Conference date: 13-06-2022 Through 17-06-2022",

year = "2022",

month = jun,

day = "9",

doi = "10.1145/3519939.3523731",

language = "English",

series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",

publisher = "Association for Computing Machinery (ACM)",

pages = "395--409",

editor = "Ranjit Jhala and Isil Dillig",

booktitle = "PLDI 2022",

address = "United States",

url = "https://pldi22.sigplan.org/",

}

Jones, EC, Ong, L & Ramsay, S 2022, CycleQ: An Efficient Basis for Cyclic Equational Reasoning. in R Jhala & I Dillig (eds), PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Association for Computing Machinery (ACM), pp. 395-409, The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, California , United States, 13/06/22. https://doi.org/10.1145/3519939.3523731

CycleQ: An Efficient Basis for Cyclic Equational Reasoning. / Jones, Eddie C; Ong, Luke; Ramsay, Steven.
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ed. / Ranjit Jhala; Isil Dillig. Association for Computing Machinery (ACM), 2022. p. 395-409 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - CycleQ

T2 - The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation

AU - Jones, Eddie C

AU - Ong, Luke

AU - Ramsay, Steven

N1 - Funding Information: We gratefully acknowledge the support of the Engineering and Physical Sciences Research Council (EP/T006579/1, EP/T006595/1) and the National Centre for Cyber Security via the UK Research Institute in Verified Trustworthy Software Systems. Publisher Copyright: © 2022 ACM.

PY - 2022/6/9

Y1 - 2022/6/9

N2 - We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proofs and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, implemented as a GHC plugin, shows promising results on a number of standard benchmarks.

AB - We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proofs and equational reasoning are mediated by the use of contextual substitution as a cut rule. We show that our system, although simple, already subsumes several of the approaches to implicit induction variously known as “inductionless induction”, “rewriting induction”, and “proof by consistency”. By restricting the form of the traces, we show that global correctness in our system can be verified incrementally, taking advantage of the well-known size-change principle, which leads to an efficient implementation of proof search. Our CycleQ tool, implemented as a GHC plugin, shows promising results on a number of standard benchmarks.

KW - Theory of computation

KW - Equational logic and rewriting

KW - Logic and verification.

U2 - 10.1145/3519939.3523731

DO - 10.1145/3519939.3523731

M3 - Conference Contribution (Conference Proceeding)

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 395

EP - 409

BT - PLDI 2022

A2 - Jhala, Ranjit

A2 - Dillig, Isil

PB - Association for Computing Machinery (ACM)

Y2 - 13 June 2022 through 17 June 2022

ER -

Jones EC, Ong L, Ramsay S. CycleQ: An Efficient Basis for Cyclic Equational Reasoning. In Jhala R, Dillig I, editors, PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery (ACM). 2022. p. 395-409. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). doi: 10.1145/3519939.3523731

CycleQ: An Efficient Basis for Cyclic Equational Reasoning

Abstract

Publication series

Conference

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Projects

8030 EPSRC EP/T006595/1 Higher-order Constrained Horn Clauses

Cite this