A theorem prover for Boolean BI

DOI10.1145/2429069.2429095MaRDI QIDQ2931798zbMATH OpenOpenAlexFDO

Authors Jong Hyun Park, Jeongbong Seo, Sungwoo Park

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.259.8072

zbMATH Keywords

Boolean bunched implicationsnested sequent calculusseparation logictheorem prover

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A theorem prover for a computational logic
• scientific article; zbMATH DE number 4164171
• scientific article; zbMATH DE number 1471980
• scientific article; zbMATH DE number 1828003
• On Model Checking Boolean BI
• scientific article; zbMATH DE number 2242591
• A proof-theoretic study of bi-intuitionistic propositional sequent calculus
• scientific article; zbMATH DE number 7359406
• A new method for the Boolean ring based theorem proving
• scientific article; zbMATH DE number 432735

Cited in

(3)

• Proof tactics for assertions in separation logic
• Completeness for a first-order abstract separation logic
• A complete axiomatisation for quantifier-free separation logic

Describes a project that uses

Uses Software

• jStar
• VeriFast

This page was built for publication: A theorem prover for Boolean BI

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931798)