Previous Up

References

[Bae08a]
David Baelde. A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique, December 2008.
[Bae08b]
David Baelde. On the expressivity of minimal generic quantification. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228, pages 3–19, 2008.
[Bae12]
David Baelde. Least and greatest fixed points in linear logic. 13(1), January 2012. ACM Transactions on Computational Logic.
[Gac10]
Andrew Gacek. The Abella interactive theorem prover – version 1.3.5, September 2010. Available from http://abella-prover.org/.
[GHN+08]
Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, and Zach Snow. The Teyjus system – version 2, March 2008. Available from http://teyjus.cs.umn.edu/.
[Gir92]
Jean-Yves Girard. A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu, February 1992.
[GJ03]
Andrew D. Gordon and Alan Jeffrey. Typing correspondence assertions for communication protocols. Theoretical Computer Science, 300(1-3):379–409, 2003.
[GMN10]
Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. Accepted to the J. of Automated Reasoning, August 2010.
[GMN11]
Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48–73, 2011.
[Mil91]
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497–536, 1991.
[Mil99]
Robin Milner. Communicating and Mobile Systems : The π-calculus. Cambridge University Press, New York, NY, USA, 1999.
[Mil00]
Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et. al., editors, Computational Logic - CL 2000, number 1861 in LNAI, pages 239–253. Springer, 2000.
[Mil06]
Dale Miller. Representing and reasoning with operational semantics. In U. Furbach and N. Shankar, editors, Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 4130 of LNAI, pages 4–20, August 2006.
[MMP03]
Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theoretical Computer Science, 294(3):411–437, 2003.
[MN87]
Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379–388, San Francisco, September 1987.
[MPW93]
Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Theoretical Computer Science, 114(1):149–171, 1993.
[MT03]
Alberto Momigliano and Alwen Tiu. Induction and co-induction in sequent calculus. In Mario Coppo Stefano Berardi and Ferruccio Damiani, editors, Post-proceedings of TYPES 2003, number 3085 in LNCS, pages 293 – 308, January 2003.
[MT05]
Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749–783, October 2005.
[Nad99]
Gopalan Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March 1999.
[Nig08]
Vivek Nigam. Using tables to construct non-redundant proofs. In C. Dimitracopoulos In A. Beckmann and B. Loewe, editors, CiE 2008: Abstracts and extended abstracts of unpublished papers, pages 354–363, 2008.
[Nip93]
Tobias Nipkow. Functional unification of higher-order patterns. In M. Vardi, editor, Proc. 8th IEEE Symposium on Logic in Computer Science (LICS 1993), pages 64–74. IEEE, June 1993.
[NL05]
Gopalan Nadathur and Natalie Linnell. Practical higher-order pattern unification with on-the-fly raising. In ICLP 2005: 21st International Logic Programming Conference, volume 3668 of LNCS, pages 371–386, Sitges, Spain, October 2005. Springer.
[NM88]
Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810–827, Seattle, August 1988. MIT Press.
[NM99]
Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus—a compiler and abstract machine based implementation of Lambda Prolog. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, pages 287–291, Trento, Italy, July 1999. Springer-Verlag LNCS.
[PE88]
Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.
[Pie05]
Brigitte Pientka. Tabling for higher-order logic programming. In 20th International Conference on Automated Deduction, Talinn, Estonia, pages 54 – 69. Springer-Verlag, 2005.
[RRR+97]
Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Terrance Swift, and David Scott Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV97), number 1254 in LNCS, pages 143–154, 1997.
[SH93]
Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Eighth Annual Symposium on Logic in Computer Science, pages 222–232. IEEE Computer Society Press, IEEE, June 1993.
[Tiu04]
Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University, May 2004.
[Tiu05]
Alwen Tiu. Model checking for π-calculus using proof search. In Martín Abadi and Luca de Alfaro, editors, CONCUR, volume 3653 of LNCS, pages 36–50. Springer, 2005.
[Tiu06]
Alwen Tiu. A logic for reasoning about generic judgments. In A. Momigliano and B. Pientka, editors, International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP’06), 2006.
[TM04]
Alwen Tiu and Dale Miller. A proof search specification of the π-calculus. In 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pages 79–101, September 2004.
[TM10]
Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2), 2010.
[TNM05]
Alwen Tiu, Gopalan Nadathur, and Dale Miller. Mixing finite success and finite failure in an automated prover. In Proceedings of ESHOL’05: Empirically Successful Automated Reasoning in Higher-Order Logics, pages 79 – 98, December 2005.

Any paper listed above that was written by one of the authors of this guide can be found on their respective home pages.


Previous Up