References

@article{abel-structuralrecanalysis,
author = {Andreas Abel and Thorsten Altenkirch},
title = {A predicative analysis of structural recursion},
journal = {J. Funct. Program.},
publisher = {Cambridge University Press},
year = {2002},
volume = {12},
number = {1},
pages = {1--41},
doi = {http://dx.doi.org/10.1017/S0956796801004191}
}

@article{Abr02,
author = {Samson Abramsky},
title = {Algorithmic game semantics: a tutorial introduction. },
publisher = {Proceedings of 2001 Marktoberdorf International Summer School, 2002.},
year = {2001}
}

@inproceedings{abramsky:mchecking_ia,
author = {Samson Abramsky},
title = {Semantics via game theory},
booktitle = {Marktoberdorf International Summer School},
year = {2001},
note = {Lecture slides}
}

@article{agom2003,
author = {S. Abramsky and D. R. Ghica and L. Ong and A. Murawski},
title = {Algorithmic Game Semantics and Component-Based Verification},
booktitle = {Proceedings of SAVBCS 2003: Specification and Verification of Component-Based Systems, Workshop at ESEC/FASE 2003},
year = {2003},
pages = {66-74},
note = {published as Technical Report 03-11, Department of Computer Science, Iowa State University},
url = {http://www.cs.iastate.edu/~leavens/SAVBCS/2003/papers/SAVCBS03.pdf}
}

@inproceedings{Abramsky1998,
author = {Abramsky, S. and Honda, K. and McCusker, G.},
title = {A fully abstract game semantics for general references},
booktitle = {Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on},
year = {1998},
pages = {334--344},
doi = {http://dx.doi.org/10.1109/LICS.1998.705669}
}

@inproceedings{DBLP:conf/lics/AbramskyHM98,
author = {Samson Abramsky and Kohei Honda and Guy McCusker},
title = {A Fully Abstract Game Semantics for General References.},
booktitle = {LICS},
year = {1998},
pages = {334-344}
}

@article{DBLP:journals/apal/AbramskyJ05,
author = {Samson Abramsky and Radha Jagadeesan},
title = {A game semantics for generic polymorphism.},
journal = {Ann. Pure Appl. Logic},
year = {2005},
volume = {133},
number = {1-3},
pages = {3-37}
}

@inproceedings{abramsky92games,
author = {Samson Abramsky and Radha Jagadeesan},
title = {Games and Full Completeness for Multiplicative Linear Logic},
booktitle = {Foundations of Software Technology and Theoretical Computer Science (FST-TCS'92)},
year = {1992},
pages = {291-301},
url = {citeseer.ist.psu.edu/article/abramsky94games.html}
}

@inproceedings{abramsky94full,
author = {Samson Abramsky and Pasquale Malacaria and Radha Jagadeesan},
title = {Full Abstraction for PCF},
booktitle = {Theoretical Aspects of Computer Software},
year = {1994},
pages = {1-15},
url = {citeseer.ist.psu.edu/abramsky95full.html}
}

@article{abramsky99full,
author = {Samson Abramsky and Guy McCusker},
title = {Full abstraction for Idealized Algol with passive expressions},
journal = {Theoretical Computer Science},
year = {1999},
volume = {227},
number = {1--2},
pages = {3--42},
url = {citeseer.ist.psu.edu/abramsky98full.html}
}

@inproceedings{abramsky98callbyvalue,
author = {Samson Abramsky and Guy McCusker},
title = {Call-by-Value Games},
booktitle = {Computer Science Logic: 11th International Workshop Proceedings},
publisher = {Springer-Verlag},
year = {1998},
url = {citeseer.ist.psu.edu/abramsky97callbyvalue.html}
}

@inproceedings{abramsky:game-semantics-tutorial,
author = {Samson Abramsky and Guy McCusker},
title = {Game Semantics},
booktitle = {Logic and Computation: Proceedings of the 1997 Marktoberdorf Summer School},
publisher = {Springer-Verlag},
year = {1998},
note = {Lecture notes}
}

@inproceedings{AM97a,
author = {Samson Abramsky and Guy McCusker},
title = {Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressions},
booktitle = {Algol-like languages},
publisher = {Birkhaüser},
year = {1997}
}

@inproceedings{Abramsky1999,
author = {Abramsky, S. and Mellies, P.-A.},
title = {Concurrent games and full completeness},
booktitle = {Logic in Computer Science, 1999. Proceedings. 14th Symposium on},
year = {1999},
pages = {431--442},
doi = {http://dx.doi.org/10.1109/LICS.1999.782638}
}

@inproceedings{DBLP:conf/fossacs/AehligMO05,
author = {Klaus Aehlig and Jolie G. de Miranda and C.-H. Luke Ong},
title = {Safety Is not a Restriction at Level 2 for String Languages.},
booktitle = {FoSSaCS},
year = {2005},
pages = {490-504}
}

@inproceedings{DBLP:conf/tlca/AehligMO05,
author = {Klaus Aehlig and Jolie G. de Miranda and C.-H. Luke Ong},
title = {The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable.},
booktitle = {TLCA},
year = {2005},
pages = {39-54}
}

@techreport{safety-mirlong2004,
author = {Klaus Aehlig and Jolie G. de Miranda and C.-H. Luke Ong},
title = {Safety is not a restriction at Level 2 for string languages},
year = {2004}
}

@article{Aho68,
author = {Alfred V. Aho},
title = {Indexed Grammars -- An Extension of Context-Free Grammars},
journal = {J. ACM},
publisher = {ACM Press},
year = {1968},
volume = {15},
number = {4},
pages = {647--671},
doi = {http://doi.acm.org/10.1145/321479.321488}
}

@inproceedings{alur-vpa,
author = {Rajeev Alur and P. Madhusudan},
title = {Visibly pushdown languages},
booktitle = {STOC '04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing},
publisher = {ACM Press},
year = {2004},
pages = {202--211},
doi = {http://doi.acm.org/10.1145/1007352.1007390}
}

@misc{asperti-np,
author = {Andrea Asperti},
title = {P = NP, up to sharing},
url = {citeseer.ist.psu.edu/133314.html}
}

@inproceedings{DBLP:conf/lics/AspertiDLR94,
author = {Andrea Asperti and Vincent Danos and Cosimo Laneve and Laurent Regnier},
title = {Paths in the lambda-calculus},
booktitle = {LICS},
year = {1994},
pages = {426-436}
}

@inbook{Barendregt:92,
author = {Henk Barendregt},
title = {Handbook of Logic in Computer Science},
publisher = {Clarendon Press},
year = {1992},
pages = {117-309}
}

@book{Barendregt84,
author = {Hendrik Pieter Barendregt},
title = {The Lambda Calculus -- Its Syntax and Semantics},
publisher = {North-Holland},
year = {1984},
volume = {103}
}

@phdthesis{gberry-thesis,
author = {Gérard Berry},
title = {Modèles Complément Adéquats et Stable des Lambda-calculs typés.},
school = {Université Paris VII},
year = {1979}
}

@inproceedings{berry-stable,
author = {Gérard Berry},
title = {Stable Models of Typed lambda-Calculi},
booktitle = {Proceedings of the Fifth Colloquium on Automata, Languages and Programming},
publisher = {Springer-Verlag},
year = {1978},
pages = {72--89}
}

@article{biere99symbolic,
author = {Armin Biere and Alessandro Cimatti and Edmund Clarke and Yunshan Zhu},
title = {Symbolic Model Checking without BDDs},
journal = {Lecture Notes in Computer Science},
year = {1999},
volume = {1579},
pages = {193--207},
url = {citeseer.ist.psu.edu/article/biere99symbolic.html}
}

@phdthesis{Blumphd,
author = {William Blum},
title = {The Safe Lambda Calculus},
school = {University of Oxford},
note = {forthcoming.}
}

@misc{Blum2008,
author = {William Blum},
title = {A tool for constructing structures generated by higher-order recursion schemes and collapsible pushdown automata},
year = {2008},
url = {web.comlab.ox.ac.uk/oucl/work/william.blum/}
}

@misc{blumtransfer,
author = {William Blum},
title = {PRS Transfer thesis},
year = {2006},
url = {http://web.comlab.ox.ac.uk/oucl/work/william.blum/mscthesis.pdf}
}

@mastersthesis{blum-mscthesis,
author = {William Blum},
title = {Termination Analysis of $-calculus and a subset of core ML},
school = {University of Oxford},
year = {2004}
}

@unpublished{localbeta2008,
author = {W. Blum and C.-H. L. Ong},
title = {Local computation of beta-reduction},
year = {2008},
note = {Work In progress.}
}

@inproceedings{blumong:safelambdacalculus,
author = {William Blum and C.-H. Luke Ong},
title = {The Safe Lambda Calculus},
booktitle = {TLCA},
year = {2007},
pages = {39-53}
}

@article{Cau02,
author = {Didier Caucal},
title = {On Infinite Terms Having a Decidable Monadic Theory},
booktitle = {MFCS '02: Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science},
publisher = {Springer-Verlag},
year = {2002},
pages = {165--176}
}

@inproceedings{Chadha2004,
author = {Chadha, R. and Kramer, S. and Scedrov , A.},
title = {Formal analysis of multi-party contract signing},
booktitle = {Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE},
year = {2004},
pages = {266--279},
doi = {http://dx.doi.org/10.1109/CSFW.2004.1310746}
}

@inproceedings{Chroboczek2000,
author = {Chroboczek, J.},
title = {Game semantics and subtyping},
booktitle = {Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on},
year = {2000},
pages = {192--203},
doi = {http://dx.doi.org/10.1109/LICS.2000.855769}
}

@inproceedings{CAV02:nusmv,
author = {A. Cimatti and E. Clarke and E. Giunchiglia and F. Giunchiglia and M. Pistore and M. Roveri and R. Sebastiani and A. Tacchella},
title = {NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking},
booktitle = {Proc. International Conference on Computer-Aided Verification (CAV 2002)},
publisher = {Springer},
year = {2002},
volume = {2404}
}

@article{ckos2005,
author = { Clarke, Edmund and Kroening, Daniel and Ouaknine, Joel and Strichman, Ofer },
title = { Computational Challenges in Bounded Model Checking },
journal = { Software Tools for Technology Transfer (STTT) },
publisher = { Springer Verlag },
year = { 2005 },
volume = { 7 },
number = { 2 },
pages = { 174--183 }
}

@article{Minsky64,
author = {John Cocke and Marvin Minsky},
title = {Universality of Tag Systems with P = 2},
journal = {J. ACM},
publisher = {ACM},
year = {1964},
volume = {11},
number = {1},
pages = {15--20},
doi = {http://doi.acm.org/10.1145/321203.321206}
}

@book{CroleRL:catt,
author = {Crole, Roy},
title = {Categories for Types},
publisher = {Cambridge University Press},
year = {1993}
}

@article{Dam82,
author = {W. Damm},
title = {The IO- and OI-hierarchy},
journal = {TCS},
year = {1982},
volume = {20},
pages = {95-207}
}

@article{DG86,
author = {Werner Damm and Andreas Goerdt},
title = {An automata-theoretical characterization of the OI-hierarchy},
journal = {Information and Control},
publisher = {Academic Press Professional, Inc.},
year = {1986},
volume = {71},
number = {1-2},
pages = {1--32},
doi = {http://dx.doi.org/10.1016/S0019-9958(86)80016-X}
}

@inproceedings{Danos2000,
author = {Danos, V. and Harmer, R.},
title = {Probabilistic game semantics},
booktitle = {Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on},
year = {2000},
pages = {204--213},
doi = {http://dx.doi.org/10.1109/LICS.2000.855770}
}

@inproceedings{Danos1996,
author = {Danos, V. and Herbelin, H. and Regnier, L.},
title = {Game semantics and abstract machines},
booktitle = {Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on},
year = {1996},
pages = {394--405},
doi = {http://dx.doi.org/10.1109/LICS.1996.561456}
}

@misc{danos-head,
author = {Vincent Danos and Laurent Regnier},
title = {Head Linear Reduction},
url = {citeseer.ist.psu.edu/danos04head.html}
}

@inproceedings{DanosRegnier-Localandasynchronou,
author = {Vincent Danos and Laurent Regnier},
title = {Local and asynchronous beta-reduction (an analysis of Girard's execution formula) },
booktitle = {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, LICS 1993},
publisher = {IEEE Computer Society Press},
year = {1993},
pages = {296--306}
}

@inproceedings{DBLP:conf/sas/DimovskiGL05,
author = {Aleksandar Dimovski and Dan R. Ghica and Ranko Lazic},
title = {Data-Abstraction Refinement: A Game Semantic Approach.},
booktitle = {SAS},
publisher = {Springer},
year = {2005},
volume = {3672},
pages = {102-117},
url = {http://dblp.uni-trier.de/db/conf/sas/sas2005.html#DimovskiGL05}
}

@inproceedings{Faggian2005,
author = {Faggian, C. and Maurel, F.},
title = {Ludics nets, a game model of concurrent interaction},
booktitle = {Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on},
year = {2005},
pages = {376--385},
doi = {http://dx.doi.org/10.1109/LICS.2005.25}
}

@article{DBLP:journals/jacm/FortuneLO83,
author = {Steven Fortune and Daniel Leivant and Michael O'Donnell},
title = {The Expressiveness of Simple and Second-Order Type Structures},
journal = {J. ACM},
year = {1983},
volume = {30},
number = {1},
pages = {151-185}
}

@article{Ghica2003,
author = {Ghica, Dan R. and McCusker, Guy},
title = {The regular-language semantics of second-order Idealized Algol},
journal = {Theoretical Computer Science},
year = {2003},
volume = {309},
number = {1-3},
pages = {469--502},
url = {http://www.sciencedirect.com/science/article/B6V1G-48R1NCH-3/1/8bc4b8ecafe0e4e3ab6af0118f30418d}
}

@inproceedings{ghicamccusker00,
author = {Dan R. Ghica and Guy McCusker},
title = {Reasoning about Idealized sc Algol Using Regular Languages},
booktitle = {Proceedings of 27th International Colloquium on Automata, Languages and Programming ICALP 2000},
publisher = {Springer-Verlag},
year = {2000},
volume = {1853},
pages = {103--116},
url = {citeseer.ist.psu.edu/ghica00reasoning.html}
}

@misc{gordonfuncprog,
author = {Mike Gordon},
title = {Introduction to Functional Programming},
year = {1996},
url = {http://www.cl.cam.ac.uk/~mjcg/Teaching/FuncProg/Notes/Notes.ps.gz}
}

@phdthesis{willgreenlandthesis,
author = {Will Greenland},
title = {Game Semantics for Region Analysis.},
school = {University of Oxford},
year = {2004}
}

@article{hmos-lics08,
author = {M. Hague and A. S. Murawski and C.-H. L. Ong and O. Serre.},
title = {Collapsible pushdown automata and recursive schemes.},
journal = {LICS},
year = {2008}
}

@inproceedings{hague-sto07,
author = {M. Hague and A. S. Murawski and C.-H. L. Ong and O. Serre.},
title = {Collapsible pushdown automata and recursive schemes.},
year = {2006},
note = {13 pages, preprint}
}

@inproceedings{hammer:truly,
author = {Moritz Hammer and Alexander Knapp and Stephan Merz},
title = {Truly On-The-Fly LTL Model Checking},
booktitle = {11th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005)},
publisher = {Springer-Verlag},
year = {2005},
pages = {191--205}
}

@inproceedings{Harding2003,
author = {Harding, A. and Ryan, M. and Schobbens, P.-Y.},
title = {Towards symbolic strategy synthesis for -LTL},
booktitle = {Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings. 10th International Symposium on},
year = {2003},
pages = {137--146}
}

@misc{Harmer2005,
author = {Russ Harmer},
title = {Innocent game semantics},
year = {2005},
note = {Course notes}
}

@inproceedings{Harmer1999,
author = {Harmer, R. and McCusker, G.},
title = {A fully abstract game semantics for finite nondeterminism},
booktitle = {Logic in Computer Science, 1999. Proceedings. 14th Symposium on},
year = {1999},
pages = {422--430},
doi = {http://dx.doi.org/10.1109/LICS.1999.782637}
}

@article{henkin1963tpt,
author = {Henkin, L.},
title = {A theory of propositional types},
journal = {Fundamenta Mathematicae},
year = {1963},
volume = {52},
number = {323-344},
pages = {2}
}

@book{Hindley1997,
author = {J. Roger Hindley},
title = {Basic simple type theory},
publisher = {Cambridge University Press},
year = {1997}
}

@book{DBLP:books/cu/HindleyS86,
author = {J. Roger Hindley and Jonathan P. Seldin},
title = {Introduction to Combinators and Lambda-Calculus},
publisher = {Cambridge University Press},
year = {1986}
}

@book{Hoa85,
author = { C. A. R. Hoare},
title = {Communicating Sequential Processes},
publisher = {Prentice-Hall},
year = {1985}
}

@article{hoare_csp,
author = {C. A. R. Hoare},
title = {Communicating sequential processes},
journal = {Commun. ACM},
publisher = {ACM Press},
year = {1983},
volume = {26},
number = {1},
pages = {100--106},
doi = {http://doi.acm.org/10.1145/357980.358021}
}

@article{honda99gametheoretic,
author = {Kohei Honda and Nobuko Yoshida},
title = {Game-theoretic analysis of call-by-value computation},
journal = {Theoretical Computer Science},
year = {1999},
volume = {221},
number = {1--2},
pages = {393--456},
url = {citeseer.ist.psu.edu/article/honda97game.html}
}

@phdthesis{huet76,
author = {Gérard P. Huet},
title = {Résolution d'équations dans des langages d'ordre 1,2,...,$},
school = {Université Paris VII},
year = {1976}
}

@article{DBLP:journals/tcs/Huet75,
author = {Gérard P. Huet},
title = {A Unification Algorithm for Typed lambda-Calculus.},
journal = {Theor. Comput. Sci.},
year = {1975},
volume = {1},
number = {1},
pages = {27-57}
}

@article{hylandong_pcf,
author = {J. M. E. Hyland and C.-H. L. Ong},
title = {On full abstraction for PCF: I, II, and III},
journal = {Information and Computation},
publisher = {Academic Press, Inc.},
year = {2000},
volume = {163},
number = {2},
pages = {285--408},
doi = {http://dx.doi.org/10.1006/inco.2000.2917}
}

@unpublished{HO93a,
author = {J. M. E. Hyland and C.-H. L. Ong},
title = {Fair Games and Full Completeness for Multiplicative Linear Logic without the MIX-Rule},
year = {1993},
note = {preprint}
}

@misc{ocaml,
author = {INRIA},
title = {Objective Caml Programming language },
year = {2003},
note = { http://caml.inria.fr/}
}

@article{DBLP:journals/tcs/JensenP76,
author = {D. C. Jensen and Tomasz Pietrzykowski},
title = {Mechanizing it mega-Order Type Theory Through Unification.},
journal = {Theor. Comput. Sci.},
year = {1976},
volume = {3},
number = {2},
pages = {123-171}
}

@inproceedings{DBLP:conf/tlca/Joly01,
author = {Thierry Joly},
title = {The Finitely Generated Types of the lambda-Calculus.},
booktitle = {TLCA},
year = {2001},
pages = {240-252}
}

@article{interpreter-spec-jones,
author = {Jones, N.D.},
title = {Transformation by interpreter specialisation},
journal = {Science of Computer Programming},
year = {2004},
volume = {52},
pages = {307--339}
}

@unpublished{jones04,
author = {N.D. Jones and N. Bohr.},
title = {Termination of the untyped lambda calculus},
year = {2004}
}

@inproceedings{KNU02,
author = {T.~Knapik and D.~Niwiński and P.~Urzyczyn},
title = {Higher-order pushdown trees are easy},
booktitle = {FOSSACS'02},
publisher = {Springer},
year = {2002},
pages = {205-222},
note = {LNCS Vol.~2303}
}

@book{KnuthAOC1,
author = {Donald E. Knuth},
title = {Fundamental Algorithms},
publisher = {Addison-Wesley},
year = {2000},
volume = {1},
edition = {Third}
}

@article{compiler-correct-jones-et-al,
author = {Lacey, D. and Jones, N.D. and Van Wyk, E. and Frederiksen, C.C.},
title = {Compiler optimization correctness by temporal logic},
journal = {Higher Order and Symbolic Computation},
year = {2004},
volume = {17},
number = {3},
pages = {173--206}
}

@inproceedings{Lafont1991,
author = {Lafont, Y. and Streicher, T.},
title = {Games semantics for linear logic},
booktitle = {Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on},
year = {1991},
pages = {43--50},
doi = {http://dx.doi.org/10.1109/LICS.1991.151629}
}

@inproceedings{Laird2001,
author = {Laird, J.},
title = {A fully abstract game semantics of local exceptions},
booktitle = {Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on},
year = {2001},
pages = {105--114},
doi = {http://dx.doi.org/10.1109/LICS.2001.932487}
}

@inproceedings{Lamarche1995,
author = {Lamarche, F.},
title = {Games semantics for full propositional linear logic},
booktitle = {Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on},
year = {1995},
pages = {464--473},
doi = {http://dx.doi.org/10.1109/LICS.1995.523280}
}

@article{lambek1986ccc,
author = {Lambek, J.},
title = {Cartesian closed categories and typed lambda-calculi},
journal = {Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages table of contents},
publisher = {Springer-Verlag New York, Inc. New York, NY, USA},
year = {1986},
pages = {136--175}
}

@inproceedings{lamping,
author = {John Lamping},
title = {An algorithm for optimal lambda calculus reduction},
booktitle = {POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
publisher = {ACM Press},
year = {1990},
pages = {16--30},
doi = {http://doi.acm.org/10.1145/96709.96711}
}

@article{jones01,
author = {C.S. Lee and N.D. Jones and A. M. Ben-Amram},
title = {The size-change principle for program termination},
publisher = {Proceedings ACM Symposium on Principles of Programming Languages},
year = {2001}
}

@article{DBLP:journals/tcs/Leivant93,
author = {Daniel Leivant},
title = {Functions Over Free Algebras Definable in the Simply Typed lambda Calculus},
journal = {Theor. Comput. Sci.},
year = {1993},
volume = {121},
number = {1&2},
pages = {309-322}
}

@inproceedings{DBLP:conf/tlca/LeivantM93,
author = {Daniel Leivant and Jean-Yves Marion},
title = {Lambda calculus characterizations of poly-time.},
booktitle = {TLCA},
year = {1993},
pages = {274-288}
}

@article{loader2001fpn,
author = {Loader, R.},
title = {Finitary PCF is not decidable},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = {2001},
volume = {266},
number = {1-2},
pages = {341--364}
}

@misc{Loader1998,
author = {Ralph Loader},
title = {Notes on Simply Typed Lambda Calculus},
year = {1998}
}

@article{loader1998upd,
author = {Loader, R.},
title = {Unary PCF is decidable},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = {1998},
volume = {206},
number = {1-2},
pages = {317--329}
}

@inproceedings{lor61,
author = {Paul Lorenzen},
title = {Ein dialogisches Konstruktivitätskriterium},
booktitle = {Infinitistic Methods.},
year = {1961},
pages = {193-200}
}

@article{mairson1992spt,
author = {Mairson, H.G.},
title = {A Simple Proof of a Theorem of Statman},
journal = {TCS},
year = {1992},
volume = {103},
number = {2},
pages = {387--394}
}

@inproceedings{Malacaria1999,
author = {Malacaria, P. and Hankin, C.},
title = {Non-deterministic games and program analysis: An application to security},
booktitle = {Logic in Computer Science, 1999. Proceedings. 14th Symposium on},
year = {1999},
pages = {443--452},
doi = {http://dx.doi.org/10.1109/LICS.1999.782639}
}

@article{Mas76,
author = {A. N. Maslov},
title = {Multilevel stack automata},
journal = {Problems of Information Transmission},
year = {1976},
volume = {12},
pages = {38--43}
}

@article{Mas74,
author = {A. N. Maslov},
title = {The hierarchy of indexed languages of an arbitrary level},
journal = {Soviet Math. Dokl.},
year = {1974},
volume = {15},
pages = {1170-1174}
}

@inproceedings{mccusker2001,
author = {Guy McCusker},
title = {On the semantics of Idealized Algol without the bad-variable constructor},
booktitle = {Nineteenth Conference on the Mathematical Foundations of Programming Semantics},
publisher = {Elsevier},
year = {2003},
volume = {83}
}

@phdthesis{McC96b,
author = {Guy McCusker},
title = {Games and Full Abstraction for a Functional Metalanguage with Recursive Types},
school = {Imperial College},
year = {1996}
}

@inproceedings{McCusker-GamesandFullAbstrac,
author = {Guy McCusker},
title = {Games and Full Abstraction for FPC},
booktitle = {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, LICS 1996},
publisher = {IEEE Computer Society Press},
year = {1996},
pages = {174-183}
}

@inproceedings{DBLP:conf/cav/McMillan03,
author = {Kenneth L. McMillan},
title = {Interpolation and SAT-Based Model Checking.},
booktitle = {CAV},
year = {2003},
pages = {1-13}
}

@inproceedings{Meyer1974,
author = {Meyer, A.R},
title = {The Inherent Computational Complexity of Theories of Ordered Sets},
booktitle = {Proc. Int'l. Cong. of Mathematicians},
year = {1974},
volume = {2},
pages = {477--482}
}

@book{Minsky67,
author = {Marvin L. Minsky},
title = {Computation: finite and infinite machines},
publisher = {Prentice-Hall, Inc.},
year = {1967}
}

@phdthesis{demirandathesis,
author = {Jolie G. de Miranda},
title = {Structures generated by higher-order grammars and the safety constraint.},
school = {University of Oxford},
year = {2006}
}

@inproceedings{Murawski2003,
author = {Murawski, A.S.},
title = {On program equivalence in languages with ground-type references},
booktitle = {Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on},
year = {2003},
pages = {108--117},
doi = {http://dx.doi.org/10.1109/LICS.2003.1210050}
}

@article{Mur04b,
author = {Andrzej S. Murawski},
title = {Games for complexity second-order call-by-name programs},
journal = {Theoretical Computer Science},
year = {2005},
note = {special issue: Game Theory meets Computer Science, accepted for publication}
}

@article{Murawski2005,
author = {Andrzej S. Murawski},
title = {About the undecidability of program equivalence in finitary languages with state},
journal = {ACM Trans. Comput. Logic},
year = {2005},
volume = {6},
pages = {701-726}
}

@article{murawski_about_2005,
author = {Andrzej S. Murawski},
title = {About the undecidability of program equivalence in finitary languages with state},
journal = {ACM Trans. Comput. Logic},
year = {2005},
volume = {6},
pages = {701-726}
}

@misc{murawski03program,
author = {Andrzej S. Murawski},
title = {On program equivalence in languages with ground-type references},
year = {2003},
url = {citeseer.ist.psu.edu/murawski03program.html}
}

@inproceedings{DBLP:conf/icalp/MurawskiOW05,
author = {Andrzej S. Murawski and C.-H. Luke Ong and Igor Walukiewicz},
title = {Idealized Algol with Ground Recursion, and DPDA Equivalence.},
booktitle = {ICALP},
year = {2005},
pages = {917-929}
}

@inproceedings{DBLP:conf/fossacs/MurawskiW05,
author = {Andrzej S. Murawski and Igor Walukiewicz},
title = {Third-Order Idealized Algol with Iteration Is Decidable.},
booktitle = {FoSSaCS},
year = {2005},
pages = {202-218},
url = {"http://www.labri.fr/publications/l3a/2005/MW05"}
}

@inproceedings{ES03,
author = {N. Eén and N. Sörensson},
title = {An Extensible SAT-solver.},
booktitle = {SAT},
year = {2003},
pages = {502-518}
}

@inproceedings{Nickau:lfcs94,
author = {Hanno Nickau},
title = {Hereditarily Sequential Functionals},
booktitle = {Proc. Symp. Logical Foundations of Computer Science: Logic at St. Petersburg},
publisher = {Springer-Verlag},
year = {1994},
volume = {813},
pages = {253--264}
}

@inproceedings{Ong2006,
author = {Ong, C.-H.L.},
title = {On Model-Checking Trees Generated by Higher-Order Recursion Schemes},
booktitle = {Logic in Computer Science, 2006 21st Annual IEEE Symposium on},
year = {2006},
pages = {81--90},
doi = {http://dx.doi.org/10.1109/LICS.2006.38}
}

@unpublished{OngHoMchecking2006,
author = {C.-H. L. Ong},
title = {On model-checking trees generated by higher-order recursion schemes (Technical report)},
year = {2006},
note = {Preprint, 42 pp},
url = {http://users.comlab. ox.ac.uk/ luke.ong/publications/ ntrees.pdf}
}

@inproceedings{OngLics2006,
author = {C.-H. L. Ong},
title = {On model-checking trees generated by higher-order recursion schemes},
booktitle = {Proceedings of IEEE Symposium on Logic in Computer Science.},
publisher = {Computer Society Press},
year = {2006},
note = {Extended abstract}
}

@unpublished{Ong2005,
author = {C.-H. L. Ong},
title = {Safe Lambda Calculus: Some Questions},
year = {2005},
note = {Note on the safe lambda calculus.}
}

@article{DBLP:journals/apal/Ong04,
author = {C.-H. Luke Ong},
title = {An approach to deciding observational equivalence of Algol-like languages.},
journal = {Ann. Pure Appl. Logic},
year = {2004},
volume = {130},
number = {1-3},
pages = {125-171}
}

@inproceedings{Ong02,
author = {C.-H. L. Ong},
title = {Observational equivalence of third-order Idealized Algol is decidable},
booktitle = {Proceedings of IEEE Symposium on Logic in Computer Science, 22-25 July 2002, Copenhagen Denmark},
publisher = {Computer Society Press},
year = {2002},
pages = {245-256},
url = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/lics02.ps.gz}
}

@article{DBLP:journals/tcs/Plotkin77,
author = {Gordon D. Plotkin},
title = {LCF Considered as a Programming Language.},
journal = {Theor. Comput. Sci.},
year = {1977},
volume = {5},
number = {3},
pages = {225-255}
}

@article{plotkin-75,
author = {Plotkin, G. D.},
title = {Call-by-name, call-by-value and the [lambda]-calculus},
journal = {Theoretical Computer Science},
year = {1975},
volume = {1},
number = {2},
pages = {125--159},
url = {http://dx.doi.org/10.1016/0304-3975(75)90017-1},
doi = {http://dx.doi.org/10.1016/0304-3975(75)90017-1}
}

@inproceedings{podelski-transpredabsrt,
author = {Andreas Podelski and Andrey Rybalchenko},
title = {Transition predicate abstraction and fair termination},
booktitle = {POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
publisher = {ACM Press},
year = {2005},
pages = {132--144},
doi = {http://doi.acm.org/10.1145/1040305.1040317}
}

@inproceedings{podelski-transinvar,
author = {Andreas Podelski and Andrey Rybalchenko},
title = {Transition Invariants},
booktitle = {LICS '04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
publisher = {IEEE Computer Society},
year = {2004},
pages = {32--41},
doi = {http://dx.doi.org/10.1109/LICS.2004.50}
}

@misc{zChaff,
author = {Princeton University},
title = {zChaff},
note = {http://www.princeton.edu/~chaff/zchaff.html+}
}

@inproceedings{Rea2004,
author = {Rea, N. and Dahyot, R. and Kokaram, A.},
title = {Modeling high level structure in sports with motion driven HMMs},
booktitle = {Acoustics, Speech, and Signal Processing, 2004. Proceedings. (ICASSP '04). IEEE International Conference on},
year = {2004},
volume = {3},
pages = {iii--621--4vol.3},
doi = {http://dx.doi.org/10.1109/ICASSP.2004.1326621}
}

@incollection{Reynolds81,
author = {John C. Reynolds},
title = {The Essence of ALGOL},
booktitle = {Algorithmic Languages},
publisher = {IFIP, North-Holland},
year = {1981},
pages = {345-372}
}

@article{schubert2001cbr,
author = {Schubert, A.},
title = {The complexity of beta-reduction in low orders},
journal = {Proceedings TLCA 2001},
publisher = {Springer},
pages = {400--414}
}

@article{schwichtenberg1991ubr,
author = {Schwichtenberg, H.},
title = {An upper bound for reduction sequences in the typed $-calculus},
journal = {Archive for Mathematical Logic},
publisher = {Springer},
year = {1991},
volume = {30},
number = {5},
pages = {405--408}
}

@article{citeulike:622637,
author = {Schwichtenberg, H.},
title = {Definierbare Funktionen im Lambda-Kalkul mit Typen},
journal = {Archiv Logik Grundlagenforsch},
year = {1976},
volume = {17},
pages = {113--114},
url = {http://citeseer.ist.psu.edu/contextsummary/598037/0}
}

@article{scott93,
author = {Dana S. Scott},
title = {A type-theoretical alternative to ISWIM, CUCH, OWHY},
journal = {Theor. Comput. Sci.},
publisher = {Elsevier Science Publishers Ltd.},
year = {1993},
volume = {121},
number = {1-2},
pages = {411--440},
doi = {http://dx.doi.org/10.1016/0304-3975(93)90095-B}
}

@unpublished{scott_lcf,
author = {Dana S. Scott},
title = {A theory of computable function of higher type},
year = {1969},
note = {Unpublished seminar notes, University of Oxford}
}

@unpublished{serenistypesct05,
author = {Damien Sereni},
title = {Simply typed $-calculus and SCT},
year = {2005},
note = {Unpublished notes}
}

@article{Statman1979,
author = {Statman, Richard},
title = {Intuitionistic propositional logic is polynomial-space complete},
journal = {Theoretical Computer Science},
year = {1979},
volume = {9},
number = {1},
pages = {67--72},
url = {http://www.sciencedirect.com/science/article/B6V1G-45FC46N-46/2/3b7ec37fdcfe223bfdf2156f099a3cec}
}

@article{Statman:1979:TLE,
author = {R. Statman},
title = {The typed lambda -calculus is not elementary recursive},
journal = {#j-THEOR-COMP-SCI#},
year = {1979},
volume = {9},
number = {1},
pages = {73--81}
}

@inproceedings{stirling02,
author = {Colin Stirling},
title = {Deciding DPDA Equivalence Is Primitive Recursive},
booktitle = {ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming},
publisher = {Springer-Verlag},
year = {2002},
pages = {821--832}
}

@article{804029,
author = {L. J. Stockmeyer and A. R. Meyer},
title = {Word problems requiring exponential time(Preliminary Report)},
booktitle = {STOC '73: Proceedings of the fifth annual ACM symposium on Theory of computing},
publisher = {ACM},
year = {1973},
pages = {1--9},
doi = {http://doi.acm.org/10.1145/800125.804029}
}

@inproceedings{Sun2005,
author = {Ji-Gui Sun and Yong-Gang Zhang},
title = {A study on parallel semantics of constraint logic programs},
booktitle = {Machine Learning and Cybernetics, 2005. Proceedings of 2005 International Conference on},
year = {2005},
volume = {4},
pages = {2182--2187Vol.4},
doi = {http://dx.doi.org/10.1109/ICMLC.2005.1527307}
}

@article{DBLP:journals/tcs/Senizergues01,
author = {Géraud Sénizergues},
title = {L(A)=L(B)? decidability results from complete formal systems.},
journal = {Theor. Comput. Sci.},
year = {2001},
volume = {251},
number = {1-2},
pages = {1-166}
}

@article{DBLP:journals/jsyml/Tait67,
author = {William Tait},
title = {Intensional Interpretations of Functionals of Finite Type I},
journal = {J. Symb. Log.},
year = {1967},
volume = {32},
number = {2},
pages = {198-212}
}

@misc{thomas97languages,
author = {W. Thomas},
title = {Languages, Automata, and Logic},
year = {1997},
url = {citeseer.ist.psu.edu/205184.html}
}

@misc{wikipedia,
author = {Wikipedia},
title = {Wikipedia, the free encyclopedia.},
year = {2004},
note = { http://en.wikipedia.org/}
}

@article{zaionc:csl94,
author = {Marek Zaionc},
title = {Lambda Representation of Operations Between Fifferent Term Algebras},
booktitle = {CSL '94: Selected Papers from the 8th International Workshop on Computer Science Logic},
publisher = {Springer-Verlag},
year = {1995},
pages = {91--105}
}

@article{DBLP:journals/apal/Zaionc91,
author = {Marek Zaionc},
title = {Lambda-Definability on Free Algebras},
journal = {Ann. Pure Appl. Logic},
year = {1991},
volume = {51},
number = {3},
pages = {279-300}
}

@article{702481,
author = {Marek Zaionc},
title = {On the "lambda"-definable tree operations},
booktitle = {Proceedings of the Conference on Algebraic Logic and Universal Algebra in Computer Science},
publisher = {Springer-Verlag},
year = {1990},
pages = {279--292}
}

@inproceedings{DBLP:conf/aluacs/Zaionc88,
author = {Marek Zaionc},
title = {On the "lambda"-definable tree operations},
booktitle = {Algebraic Logic and Universal Algebra in Computer Science},
year = {1988},
pages = {279-292}
}

@article{DBLP:journals/tcs/Zaionc87,
author = {Marek Zaionc},
title = {Word Operation Definable in the Typed lambda-Calculus},
journal = {Theor. Comput. Sci.},
year = {1987},
volume = {52},
pages = {1-14}
}

@proceedings{DBLP:conf/tlca/2007,,
title = {Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings},
booktitle = {TLCA},
publisher = {Springer},
year = {2007},
volume = {4583}
}

@proceedings{DBLP:conf/fossacs/2005,,
title = {Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings},
booktitle = {FoSSaCS},
publisher = {Springer},
year = {2005},
volume = {3441}
}

@proceedings{DBLP:conf/icalp/2005,,
title = {Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings},
booktitle = {ICALP},
publisher = {Springer},
year = {2005},
volume = {3580}
}

@proceedings{DBLP:conf/sas/2005,,
title = {Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings},
booktitle = {SAS},
publisher = {Springer},
year = {2005},
volume = {3672}
}

@proceedings{DBLP:conf/tlca/2005,,
title = {Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings},
booktitle = {TLCA},
publisher = {Springer},
year = {2005},
volume = {3461}
}

@proceedings{DBLP:conf/cav/2003,,
title = {Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
booktitle = {CAV},
publisher = {Springer},
year = {2003},
volume = {2725}
}

@proceedings{DBLP:conf/lics/LICS9,,
title = {Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, 4-7 July 1994, Paris, France},
booktitle = {LICS},
publisher = {IEEE Computer Society},
year = {1994}
}

@proceedings{DBLP:conf/tlca/1993,,
title = {Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings},
booktitle = {TLCA},
publisher = {Springer},
year = {1993},
volume = {664}
}