Publications
Recent draft
Refereed journal and conference/workshop proceedings
2008
2007
- Classical Modal Display Logic in the
Calculus of Structures and Minimal Cut-free Deep Inference Calculi for
S5.
Joint work with Rajeev Gore. Journal of Logic and
Computation, volume 17, number 4, pages 767 - 794, 2007.
- A trace based bisimulation for
the spi-calculus: an extended abstract. In Proceedings of APLAS 2007, LNCS 4807,
pages 367 - 382, 2007. © Copyright Springer-Verlag.
- Verification of Clock Synchronization
Algorithms: Experiments on a combination of deductive tools. Joint
work with Damian Barsotti and Leonor Prensa Nieto. Formal Aspects of
Computing, volume 19, number 3, Springer, 2007. © Copyright Springer-Verlag.
- The Bedwyr system for model checking
over
syntactic expressions. Joint work with David Baelde, Andrew Gacek,
Dale Miller and Gopalan Nadathur. In Proceedings of CADE
2007, LNAI 4603, pages 391-397. Springer, 2007. © Copyright Springer-Verlag.
- A Logic for Reasoning about Generic Judgments.
In Proceedings of LFMTP'06, volume 174, issue 5, ENTCS, pages 3 - 18,
Elsevier, 2007. This is a revised
version of the article in the proceedings. The original article
contains a mistake in one of the examples. An extended
version is available.
2006
- A Local System for Intuitionistic
Logic. In Proceedings of LPAR 2006, Volume 4246 of LNCS, Springer,
2006. © Copyright Springer-Verlag.
An extended
version is available.
- A System of
Interaction and Structure II: the Need for Deep Inference. Logical
Methods in Computer Science, Vol. 2 (2:4) 2006, pages 1-24, April 2006.
- Expressiveness + Automation + Soundness:
Towards Combining SMT Solvers and Interactive Proof Assistants.
Joint work with Pascal Fontaine, Jean-Yves Marion, Stephan Merz and
Leonor Prensa Nieto. In the Proceedings of TACAS 2006, Volume 3920 of
LNCS, pages 167 - 181, Springer, 2006. © Copyright Springer-Verlag.
2005
- Mixing Finite Success and Finite Failure
in an Automated Prover. Joint work with Dale Miller and Gopalan Nadathur. In
the Proceedings of ESHOL'05: Emperically
Successful
Automated Reasoning
in Higher-Order Logics. December, 2005.
- Verification of Clock Synchronization
Algorithms: Experiments on a combination of deductive tools. Joint
work with Damian Barsotti and Leonor
Prensa. In Proceedings of AVOCS 2005, Volume 145 of ENTCS, pages
63-78, Elsevier, 2005.
- Model checking for pi-calculus using proof
search. In Proceedings of
CONCUR 2005, LNCS Vol. 3653, pages 36 - 50, Springer-Verlag, 2005.
© Copyright Springer-Verlag.
An extended version is available. The
implementation of the model checkers described in this paper is done in
the Level
0/1 prover. The (executable) specifications for the model checker: pi.def (specification of the transition system for
pi calculus) and modal.def (specification of
the modal logics).
- A Proof Search Specification of the
pi-Calculus.
Joint paper with Dale Miller. In Proceedings of the 3rd workshop in
Foundations of
Global Ubiquitous Computing 2004. ENTCS Vol. 138, Issue 1, pages 79 -
101, 2005. Here is an extended version
with proofs.
- A Proof
Theory for Generic Judgments.
Joint work with Dale Miller. ACM Transactions on Computational Logic,
Vol. 6, No. 4, pages 749 -
783, October 2005.
2003
2002
- Encoding generic judgments.
Joint work with Dale Miller. Proceedings of FSTTCS 2002 (22nd
Foundations of Software
Technology and Theoretical Computer Science), edited by M. Agrawal and
A. Seth (PDF,
DVI).
© Copyright Springer-Verlag.
2001
Thesis
- Properties of a Logical System in the Calculus of Structures. [ps.gz
, pdf
or dvi.gz]
Master Thesis, TU Dresden, July 2001. Adviser: Alessio Guglielmi. Also
available as Technical Report WV-01-06 at TU Dresden. A revised version has
appeared in the LMCS journal.
Unpublished notes & slides