Publications

Publications

Recent draft

Proof search specifications for bisimulation and modal logics for the pi-calculus. Joint work with Dale Miller. May 2008.
A proof theoretic analysis of intruder theories. Joint work with Rajeev Gore. April 2008.
A trace based bisimulation for the spi-calculus. [Extended abstract, full paper]. This is a revised and trimmed version of an earlier draft (titled: "A formulation of open bisimulation for the spi-calculus). June 2007.

Refereed journal and conference/workshop proceedings

2008

Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. Joint work with Rajeev Gore and Linda Postniece. Accepted to AiML 2008.
On the role of names in reasoning about lamda-tree syntax specifications. May 2008. To appear in the proceedings of LFMTP 2008. Some of the proofs are verified using the proof assistant Abella. Here is the proof script.

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

Induction and Co-induction in Sequent Calculus. Joint work with Alberto Momigliano. Proceedings of TYPES 2003, LNCS volume 3085, pages 293 - 308, Springer-Verlag, 2003. ©Copyright Springer-Verlag.
A proof theory for generic judgments: an extended abstract. Joint work with Dale Miller. Proceedings of LICS 2003, edited by Phokion Kolaitis. Ottawa, July 2003,pp. 118 - 127.

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

A Local System for Classical Logic.Joint work with Kai Bruennler. Proceedings of LPAR 2001, LNAI 2250, pp. 347 - 361. ©Copyright Springer-Verlag

Thesis

A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Penn State University, May 2004. Adviser: Dale Miller. A copy of my thesis is also available at http://etda.libraries.psu.edu.

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

Cut Elimination for a Logic with Generic Judgments and Induction. Contains technical proofs of the LFMTP'06 paper.
Slides for ANU Logic summer school 2007: lecture 1, lecture 2, lecture3, lecture 4, lecture 5.
Formalization of a Generalized Clock Synchronization Protocol. Isabelle/HOL proof document. Here is the Isar proof script.. Available also from Isabelle's Archive of Formal Proofs.
An Extension of L-lambda Unification. September 16, 2002. [ dvi , pdf ].