References

[Bae08a]

David Baelde.
A linear approach to the prooftheory 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 MetaLanguages: 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://abellaprover.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]

JeanYves 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(13):379–409, 2003.
 [GMN10]

Andrew Gacek, Dale Miller, and Gopalan Nadathur.
A twolevel 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 lambdaabstraction, 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 coinduction in sequent calculus.
In Mario Coppo Stefano Berardi and Ferruccio Damiani, editors, Postproceedings 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 finegrained 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 nonredundant 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 higherorder 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 higherorder pattern unification with onthefly 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.
SpringerVerlag LNCS.
 [PE88]

Frank Pfenning and Conal Elliott.
Higherorder abstract syntax.
In Proceedings of the ACMSIGPLAN Conference on Programming
Language Design and Implementation, pages 199–208. ACM Press, June 1988.
 [Pie05]

Brigitte Pientka.
Tabling for higherorder logic programming.
In 20th International Conference on Automated Deduction, Talinn,
Estonia, pages 54 – 69. SpringerVerlag, 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 SchroederHeister.
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 MetaLanguages: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 HigherOrder 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.