| Publication | Date of Publication | Type |
|---|
On the complexity of pointer arithmetic in separation logic
Programming Languages and Systems | 2023-08-02 | Paper |
| Reasoning over permissions regions in concurrent separation logic | 2021-02-09 | Paper |
Automatically verifying temporal properties of pointer programs with cyclic proof
Journal of Automated Reasoning | 2020-03-03 | Paper |
A decision procedure for satisfiability in separation logic with inductive predicates
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | 2018-04-23 | Paper |
| Realizability in cyclic proof: extracting ordering information for infinite descent | 2018-02-02 | Paper |
Automatically verifying temporal properties of pointer programs with cyclic proof
Automated Deduction – CADE 26 | 2017-09-22 | Paper |
Biabduction (and related problems) in array separation logic
(available as arXiv preprint) | 2017-09-22 | Paper |
| Biabduction (and related problems) in array separation logic | 2017-09-22 | Paper |
| Sub-classical Boolean Bunched Logics and the Meaning of Par | 2017-08-31 | Paper |
Model checking for symbolic-heap separation logic with inductive predicates
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Machine-checked interpolation theorems for substructural logics using display calculi
Automated Reasoning | 2016-09-05 | Paper |
A unified display proof theory for bunched logic
Electronic Notes in Theoretical Computer Science | 2016-07-08 | Paper |
Disproving inductive entailments in separation logic via base pair approximation
Lecture Notes in Computer Science | 2015-12-11 | Paper |
Classical BI
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
Undecidability of propositional separation logic and its neighbours
Journal of the ACM | 2014-09-12 | Paper |
Cyclic proofs of program termination in separation logic
Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
Parametric completeness for separation theories
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
The mechanisation of Barendregt-style equational proofs (the residual perspective)
Electronic Notes in Theoretical Computer Science | 2013-07-24 | Paper |
Bunched logics displayed
Studia Logica | 2013-02-18 | Paper |
Sequent calculi for induction and infinite descent
Journal Of Logic And Computation | 2011-12-19 | Paper |
Automated cyclic entailment proofs in separation logic
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Craig interpolation in displayable logics
Lecture Notes in Computer Science | 2011-07-01 | Paper |
Classical BI: Its Semantics and Proof Theory
Logical Methods in Computer Science | 2010-07-27 | Paper |
Formalised Inductive Reasoning in the Logic of Bunched Implications
Static Analysis | 2009-03-03 | Paper |
Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science | 2006-07-07 | Paper |
A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1722714 (Why is no real title available?) | 2002-03-21 | Paper |
