| Publication | Date of Publication | Type |
|---|
scientific article; zbMATH DE number 7650841 (Why is no real title available?)
(available as arXiv preprint) | 2023-02-07 | Paper |
Display to Labeled Proofs and Back Again for Tense Logics
ACM Transactions on Computational Logic | 2022-02-24 | Paper |
Display to Labeled Proofs and Back Again for Tense Logics
ACM Transactions on Computational Logic | 2022-02-24 | Paper |
scientific article; zbMATH DE number 7407774 (Why is no real title available?)
(available as arXiv preprint) | 2021-10-08 | Paper |
| scientific article; zbMATH DE number 7407774 (Why is no real title available?) | 2021-10-08 | Paper |
An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
Journal of Automated Reasoning | 2021-06-09 | Paper |
Compositional reasoning for shared-variable concurrent programs
(available as arXiv preprint) | 2021-05-04 | Paper |
| Compositional reasoning for shared-variable concurrent programs | 2021-05-04 | Paper |
Quasi-open bisimilarity with mismatch is intuitionistic
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
CSimpl: a rely-guarantee-based framework for verifying concurrent programs
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
| A characterisation of open bisimilarity using an intuitionistic modal logic | 2020-05-27 | Paper |
| Combining proverif and automated theorem provers for security protocol verification | 2020-03-10 | Paper |
Trace-length independent runtime monitoring of quantitative policies in LTL
FM 2015: Formal Methods | 2019-12-19 | Paper |
De Morgan dual nominal quantifiers modelling private names in non-commutative logic
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
De Morgan dual nominal quantifiers modelling private names in non-commutative logic
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
(available as arXiv preprint) | 2019-10-11 | Paper |
Constructing weak simulations from linear implications for processes with private names
Mathematical Structures in Computer Science | 2019-10-09 | Paper |
| Abella: a system for reasoning about relational specifications | 2019-09-18 | Paper |
A labelled sequent calculus for BBI: proof theory and proof search
Journal Of Logic And Computation | 2019-01-31 | Paper |
A labelled sequent calculus for BBI: proof theory and proof search
Journal Of Logic And Computation | 2019-01-31 | Paper |
Modular labelled sequent calculi for abstract separation logics
ACM Transactions on Computational Logic | 2018-08-10 | Paper |
Modular labelled sequent calculi for abstract separation logics
ACM Transactions on Computational Logic | 2018-08-10 | Paper |
| scientific article; zbMATH DE number 6851953 (Why is no real title available?) | 2018-03-21 | Paper |
Semantics for specialising attack trees based on linear logic
Fundamenta Informaticae | 2018-01-05 | Paper |
| Proof tactics for assertions in separation logic | 2018-01-04 | Paper |
A proof theory for generic judgments
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Annotation-free sequent calculi for full intuitionistic linear logic
(available as arXiv preprint) | 2017-02-02 | Paper |
Completeness for a first-order abstract separation logic
Programming Languages and Systems | 2016-12-21 | Paper |
On the role of names in reasoning about \(\lambda\)-tree syntax specifications
Electronic Notes in Theoretical Computer Science | 2016-05-06 | Paper |
Automated theorem proving for assertions in separation logic with all connectives
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Extracting proofs from tabled proof search
Certified Programs and Proofs | 2015-01-13 | Paper |
From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
Advanced Information Systems Engineering | 2014-09-15 | Paper |
scientific article; zbMATH DE number 6302922 (Why is no real title available?)
(available as arXiv preprint) | 2014-06-11 | Paper |
Proof search for propositional abstract separation logics via labelled sequents
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
| A logic for reasoning about generic judgments | 2014-01-10 | Paper |
| Verification of clock synchronization algorithms: experiments on a combination of deductive tools | 2013-12-04 | Paper |
A labelled sequent calculus for BBI: proof theory and proof search
Lecture Notes in Computer Science | 2013-10-04 | Paper |
| A proof search specification of the \(\pi\)-calculus | 2013-09-26 | Paper |
Cut elimination for a logic with induction and co-induction
Journal of Applied Logic | 2013-05-02 | Paper |
Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus
Formal Aspects of Computing | 2013-03-22 | Paper |
Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus
Formal Aspects of Computing | 2013-03-22 | Paper |
Stratification in logics of definitions
Automated Reasoning | 2012-09-05 | Paper |
| Cut-elimination and proof search for bi-intuitionistic tense logic | 2012-08-05 | Paper |
A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
Lecture Notes in Computer Science | 2011-07-01 | Paper |
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
Logical Methods in Computer Science | 2011-05-26 | Paper |
A Local System for Classical Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-05-06 | Paper |
| Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents | 2011-03-30 | Paper |
A proof theoretic analysis of intruder theories
Logical Methods in Computer Science | 2010-09-21 | Paper |
Taming displayed tense logics using nested sequents with deep inference
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Formalising Observer Theory for Environment-Sensitive Bisimulation
Lecture Notes in Computer Science | 2009-10-20 | Paper |
A First-Order Policy Language for History-Based Transaction Monitoring
Theoretical Aspects of Computing - ICTAC 2009 | 2009-08-20 | Paper |
A Proof Theoretic Analysis of Intruder Theories
Rewriting Techniques and Applications | 2009-06-30 | Paper |
Matching Trace Patterns with Regular Policies
Language and Automata Theory and Applications | 2009-04-02 | Paper |
A Local System for Intuitionistic Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract
Programming Languages and Systems | 2008-05-15 | Paper |
Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5
Journal Of Logic And Computation | 2007-11-19 | Paper |
A System of Interaction and Structure II: The Need for Deep Inference
Logical Methods in Computer Science | 2007-10-11 | Paper |
Verification of clock synchronization algorithms: experiments on a combination of deductive tools
Formal Aspects of Computing | 2007-09-06 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-05-02 | Paper |
CONCUR 2005 – Concurrency Theory
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2005-12-23 | Paper |
| scientific article; zbMATH DE number 1954369 (Why is no real title available?) | 2003-07-28 | Paper |
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
(available as arXiv preprint) | N/A | Paper |
