The logic Linc is an extension of the logic FOLDN by Dale Miller and Ray McDowell. You will find below various fragments of Linc during its design phases. The complete logic appears in Tiu's PhD thesis.
 |
Alwen Tiu, Gopalan Nadathur and Dale Miller. Mixing Finite Success and Finite Failure in an Automated Prover. Submitted. |
|
|
Alwen Tiu. Model Checking for pi-Calculus Using Proof Search. Proceedings of the 16th international conference on Concurrency Theory (CONCUR) 2005. |
| Alwen Tiu and Dale Miller. A Proof Search Specification of the pi-calculus. In Proceedings of the 3rd workshop in Foundations of Global Ubiquitous Computing 2004. |
| Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Penn State University, May 2004. |
| Dale Miller and Alwen Tiu. A proof theory for generic judgments. Accepted pending minor revisions for publication at a special issue of the ACM Transactions on Computational Logic, edited by Phokion Kolaitis. |
| Alberto Momigliano and Alwen Tiu. Induction and Co-induction in Sequent Calculus. Proceedings of TYPES 2003, LNCS volume 3085, pages 293 - 308, Springer-Verlag, 2003. |
Slides
A logical framework for reasoning with names. TU Dresden, 17 November 2003, Dresden, Germany.
Induction and co-induction in sequent calculus. Workshop on Proof Theory, 3 July 2003, Dresden, Germany.
A proof theory for generic judgment. LICS 2003 conference, 23 June 2003, Ottawa, Canada.