# References

Author | Title | Year | Journal/Proceedings | Reftype | DOI/URL |
---|---|---|---|---|---|

Abel, A. & Altenkirch, T. | A predicative analysis of structural recursion [BibTeX] |
2002 | J. Funct. Program. | article | DOI |

BibTeX:
@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} } |
|||||

Abramsky, S. | Algorithmic game semantics: a tutorial introduction. [BibTeX] |
2001 | article | ||

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

Abramsky, S. | Semantics via game theory [BibTeX] |
2001 | Marktoberdorf International Summer School | inproceedings | |

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

Abramsky, S., Ghica, D. R., Ong, L. & Murawski, A. | Algorithmic Game Semantics and Component-Based Verification [BibTeX] |
2003 | Proceedings of SAVBCS 2003: Specification and Verification of Component-Based Systems, Workshop at ESEC/FASE 2003 | article | URL |

BibTeX:
@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} } |
|||||

Abramsky, S., Honda, K. & McCusker, G. | A fully abstract game semantics for general references [BibTeX] |
1998 | Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Abramsky, S., Honda, K. & McCusker, G. | A Fully Abstract Game Semantics for General References. [BibTeX] |
1998 | LICS | inproceedings | |

BibTeX:
@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} } |
|||||

Abramsky, S. & Jagadeesan, R. | A game semantics for generic polymorphism. [BibTeX] |
2005 | Ann. Pure Appl. Logic | article | |

BibTeX:
@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} } |
|||||

Abramsky, S. & Jagadeesan, R. | Games and Full Completeness for Multiplicative Linear Logic [BibTeX] |
1992 | Foundations of Software Technology and Theoretical Computer Science (FST-TCS'92) | inproceedings | URL |

BibTeX:
@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} } |
|||||

Abramsky, S., Malacaria, P. & Jagadeesan, R. | Full Abstraction for PCF [BibTeX] |
1994 | Theoretical Aspects of Computer Software | inproceedings | URL |

BibTeX:
@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} } |
|||||

Abramsky, S. & McCusker, G. | Full abstraction for Idealized Algol with passive expressions [BibTeX] |
1999 | Theoretical Computer Science | article | URL |

BibTeX:
@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} } |
|||||

Abramsky, S. & McCusker, G. | Call-by-Value Games [BibTeX] |
1998 | Computer Science Logic: 11th International Workshop Proceedings | inproceedings | URL |

BibTeX:
@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} } |
|||||

Abramsky, S. & McCusker, G. | Game Semantics [BibTeX] |
1998 | Logic and Computation: Proceedings of the 1997 Marktoberdorf Summer School | inproceedings | |

BibTeX:
@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} } |
|||||

Abramsky, S. & McCusker, G. | Linearity, Sharing and State: a fully abstract game semantics for Idealized Algol with active expressions [BibTeX] |
1997 | Algol-like languages | inproceedings | |

BibTeX:
@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} } |
|||||

Abramsky, S. & Mellies, P. | Concurrent games and full completeness [BibTeX] |
1999 | Logic in Computer Science, 1999. Proceedings. 14th Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Aehlig, K., de Miranda, J. G. & Ong, C. L. | Safety Is not a Restriction at Level 2 for String Languages. [BibTeX] |
2005 | FoSSaCS | inproceedings | |

BibTeX:
@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} } |
|||||

Aehlig, K., de Miranda, J. G. & Ong, C. L. | The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. [BibTeX] |
2005 | TLCA | inproceedings | |

BibTeX:
@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} } |
|||||

Aehlig, K., de Miranda, J. G. & Ong, C. L. | Safety is not a restriction at Level 2 for string languages [BibTeX] |
2004 | techreport | ||

BibTeX:
@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} } |
|||||

Aho, A. V. | Indexed Grammars -- An Extension of Context-Free Grammars [BibTeX] |
1968 | J. ACM | article | DOI |

BibTeX:
@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} } |
|||||

Alur, R. & Madhusudan, P. | Visibly pushdown languages [BibTeX] |
2004 | STOC '04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Asperti, A. | P = NP, up to sharing [BibTeX] |
misc | URL | ||

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

Asperti, A., Danos, V., Laneve, C. & Regnier, L. | Paths in the lambda-calculus [BibTeX] |
1994 | LICS | inproceedings | |

BibTeX:
@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} } |
|||||

Barendregt, H. | Handbook of Logic in Computer Science [BibTeX] |
1992 | inbook | ||

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

Barendregt, H. P. | The Lambda Calculus -- Its Syntax and Semantics [BibTeX] |
1984 | book | ||

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

Berry, G. | Modèles Complément Adéquats et Stable des Lambda-calculs typés. [BibTeX] |
1979 | School: Université Paris VII |
phdthesis | |

BibTeX:
@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} } |
|||||

Berry, G. | Stable Models of Typed lambda-Calculi [BibTeX] |
1978 | Proceedings of the Fifth Colloquium on Automata, Languages and Programming | inproceedings | |

BibTeX:
@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} } |
|||||

Biere, A., Cimatti, A., Clarke, E. & Zhu, Y. | Symbolic Model Checking without BDDs [BibTeX] |
1999 | Lecture Notes in Computer Science | article | URL |

BibTeX:
@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} } |
|||||

Blum, W. | The Safe Lambda Calculus [BibTeX] |
School: University of Oxford |
phdthesis | ||

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

Blum, W. | A tool for constructing structures generated by higher-order recursion schemes and collapsible pushdown automata [BibTeX] |
2008 | misc | URL | |

BibTeX:
@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/} } |
|||||

Blum, W. | PRS Transfer thesis [BibTeX] |
2006 | misc | URL | |

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

Blum, W. | Termination Analysis of $-calculus and a subset of core ML | 2004 | School: University of Oxford |
mastersthesis | |

Abstract: Lee, Jones and Ben-Amram introduced ``size-change termination'', a decidable property strictly stronger than termination. They invented a method called the ``size-change principle'' to analyze it. I propose an extension of the size-change principle to a subset of ML featuring ground type values, higher-order type values and recursively defined functions. Compared to other works, this is the first time that the size-change principle is applied to a higher-order functional language.The language handles natively if-then-else and let rec structures. The resulting algorithm produces the expected result for higher-order values but can also analyze the size of ground type values. This enhances the scope of the termination analyzer to some recursively defined function operating on numbers. |
|||||

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

Blum, W. & Ong, C. L. | Local computation of beta-reduction [BibTeX] |
2008 | unpublished | ||

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

Blum, W. & Ong, C. L. | The Safe Lambda Calculus [BibTeX] |
2007 | TLCA | inproceedings | |

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

Caucal, D. | On Infinite Terms Having a Decidable Monadic Theory [BibTeX] |
2002 | MFCS '02: Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science | article | |

BibTeX:
@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} } |
|||||

Chadha, R., Kramer, S. & Scedrov, A. | Formal analysis of multi-party contract signing [BibTeX] |
2004 | Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Chroboczek, J. | Game semantics and subtyping [BibTeX] |
2000 | Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R. & Tacchella, A. | NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking [BibTeX] |
2002 | Proc. International Conference on Computer-Aided Verification (CAV 2002) | inproceedings | |

BibTeX:
@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} } |
|||||

Clarke, E., Kroening, D., Ouaknine, J. & Strichman, O. | Computational Challenges in Bounded Model Checking [BibTeX] |
2005 | Software Tools for Technology Transfer (STTT) | article | |

BibTeX:
@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 } } |
|||||

Cocke, J. & Minsky, M. | Universality of Tag Systems with P = 2 [BibTeX] |
1964 | J. ACM | article | DOI |

BibTeX:
@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} } |
|||||

Crole, R. | Categories for Types [BibTeX] |
1993 | book | ||

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

Damm, W. | The IO- and OI-hierarchy [BibTeX] |
1982 | TCS | article | |

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

Damm, W. & Goerdt, A. | An automata-theoretical characterization of the OI-hierarchy [BibTeX] |
1986 | Information and Control | article | DOI |

BibTeX:
@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} } |
|||||

Danos, V. & Harmer, R. | Probabilistic game semantics [BibTeX] |
2000 | Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Danos, V., Herbelin, H. & Regnier, L. | Game semantics and abstract machines [BibTeX] |
1996 | Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Danos, V. & Regnier, L. | Head Linear Reduction [BibTeX] |
misc | URL | ||

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

Danos, V. & Regnier, L. | Local and asynchronous beta-reduction (an analysis of Girard's execution formula) [BibTeX] |
1993 | Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, LICS 1993 | inproceedings | |

BibTeX:
@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} } |
|||||

Dimovski, A., Ghica, D. R. & Lazic, R. | Data-Abstraction Refinement: A Game Semantic Approach. [BibTeX] |
2005 | SAS | inproceedings | URL |

BibTeX:
@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} } |
|||||

Faggian, C. & Maurel, F. | Ludics nets, a game model of concurrent interaction [BibTeX] |
2005 | Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Fortune, S., Leivant, D. & O'Donnell, M. | The Expressiveness of Simple and Second-Order Type Structures [BibTeX] |
1983 | J. ACM | article | |

BibTeX:
@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} } |
|||||

Ghica, D. R. & McCusker, G. | The regular-language semantics of second-order Idealized Algol [BibTeX] |
2003 | Theoretical Computer Science | article | URL |

BibTeX:
@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} } |
|||||

Ghica, D. R. & McCusker, G. | Reasoning about Idealized sc Algol Using Regular Languages [BibTeX] |
2000 | Proceedings of 27th International Colloquium on Automata, Languages and Programming ICALP 2000 | inproceedings | URL |

BibTeX:
@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} } |
|||||

Gordon, M. | Introduction to Functional Programming [BibTeX] |
1996 | misc | URL | |

BibTeX:
@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} } |
|||||

Greenland, W. | Game Semantics for Region Analysis. [BibTeX] |
2004 | School: University of Oxford |
phdthesis | |

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

Hague, M., Murawski, A. S., Ong, C. L. & Serre., O. | Collapsible pushdown automata and recursive schemes. [BibTeX] |
2008 | LICS | article | |

BibTeX:
@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} } |
|||||

Hague, M., Murawski, A. S., Ong, C. L. & Serre., O. | Collapsible pushdown automata and recursive schemes. [BibTeX] |
2006 | inproceedings | ||

BibTeX:
@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} } |
|||||

Hammer, M., Knapp, A. & Merz, S. | Truly On-The-Fly LTL Model Checking [BibTeX] |
2005 | 11th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) | inproceedings | |

BibTeX:
@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} } |
|||||

Harding, A., Ryan, M. & Schobbens, P. | Towards symbolic strategy synthesis for -LTL [BibTeX] |
2003 | Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings. 10th International Symposium on | inproceedings | |

BibTeX:
@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} } |
|||||

Harmer, R. | Innocent game semantics [BibTeX] |
2005 | misc | ||

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

Harmer, R. & McCusker, G. | A fully abstract game semantics for finite nondeterminism [BibTeX] |
1999 | Logic in Computer Science, 1999. Proceedings. 14th Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Henkin, L. | A theory of propositional types [BibTeX] |
1963 | Fundamenta Mathematicae | article | |

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

Hindley, J. R. | Basic simple type theory [BibTeX] |
1997 | book | ||

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

Hindley, J. R. & Seldin, J. P. | Introduction to Combinators and Lambda-Calculus [BibTeX] |
1986 | book | ||

BibTeX:
@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} } |
|||||

Hoare, C. A. R. | Communicating Sequential Processes [BibTeX] |
1985 | book | ||

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

Hoare, C. A. R. | Communicating sequential processes [BibTeX] |
1983 | Commun. ACM | article | DOI |

BibTeX:
@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} } |
|||||

Honda, K. & Yoshida, N. | Game-theoretic analysis of call-by-value computation [BibTeX] |
1999 | Theoretical Computer Science | article | URL |

BibTeX:
@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} } |
|||||

Huet, Gé. P. | Résolution d'équations dans des langages d'ordre 1,2,...,$ [BibTeX] |
1976 | School: Université Paris VII |
phdthesis | |

BibTeX:
@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} } |
|||||

Huet, Gé. P. | A Unification Algorithm for Typed lambda-Calculus. [BibTeX] |
1975 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Hyland, J. M. E. & Ong, C. L. | On full abstraction for PCF: I, II, and III [BibTeX] |
2000 | Information and Computation | article | DOI |

BibTeX:
@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} } |
|||||

Hyland, J. M. E. & Ong, C. L. | Fair Games and Full Completeness for Multiplicative Linear Logic without the MIX-Rule [BibTeX] |
1993 | unpublished | ||

BibTeX:
@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} } |
|||||

INRIA | Objective Caml Programming language [BibTeX] |
2003 | misc | ||

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

Jensen, D. C. & Pietrzykowski, T. | Mechanizing it mega-Order Type Theory Through Unification. [BibTeX] |
1976 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Joly, T. | The Finitely Generated Types of the lambda-Calculus. [BibTeX] |
2001 | TLCA | inproceedings | |

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

Jones, N. | Transformation by interpreter specialisation [BibTeX] |
2004 | Science of Computer Programming | article | |

BibTeX:
@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} } |
|||||

Jones, N. & Bohr., N. | Termination of the untyped lambda calculus [BibTeX] |
2004 | unpublished | ||

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

Knapik, T., Niwiński, D. & Urzyczyn, P. | Higher-order pushdown trees are easy [BibTeX] |
2002 | FOSSACS'02 | inproceedings | |

BibTeX:
@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} } |
|||||

Knuth, D. E. | Fundamental Algorithms [BibTeX] |
2000 | book | ||

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

Lacey, D., Jones, N., Van Wyk, E. & Frederiksen, C. | Compiler optimization correctness by temporal logic [BibTeX] |
2004 | Higher Order and Symbolic Computation | article | |

BibTeX:
@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} } |
|||||

Lafont, Y. & Streicher, T. | Games semantics for linear logic [BibTeX] |
1991 | Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Laird, J. | A fully abstract game semantics of local exceptions [BibTeX] |
2001 | Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Lamarche, F. | Games semantics for full propositional linear logic [BibTeX] |
1995 | Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Lambek, J. | Cartesian closed categories and typed lambda-calculi [BibTeX] |
1986 | Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages table of contents | article | |

BibTeX:
@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} } |
|||||

Lamping, J. | An algorithm for optimal lambda calculus reduction [BibTeX] |
1990 | POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Lee, C., Jones, N. & Ben-Amram, A. M. | The size-change principle for program termination [BibTeX] |
2001 | article | ||

BibTeX:
@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} } |
|||||

Leivant, D. | Functions Over Free Algebras Definable in the Simply Typed lambda Calculus [BibTeX] |
1993 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Leivant, D. & Marion, J. | Lambda calculus characterizations of poly-time. [BibTeX] |
1993 | TLCA | inproceedings | |

BibTeX:
@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} } |
|||||

Loader, R. | Finitary PCF is not decidable [BibTeX] |
2001 | Theoretical Computer Science | article | |

BibTeX:
@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} } |
|||||

Loader, R. | Notes on Simply Typed Lambda Calculus [BibTeX] |
1998 | misc | ||

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

Loader, R. | Unary PCF is decidable [BibTeX] |
1998 | Theoretical Computer Science | article | |

BibTeX:
@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} } |
|||||

Lorenzen, P. | Ein dialogisches Konstruktivitätskriterium [BibTeX] |
1961 | Infinitistic Methods. | inproceedings | |

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

Mairson, H. | A Simple Proof of a Theorem of Statman [BibTeX] |
1992 | TCS | article | |

BibTeX:
@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} } |
|||||

Malacaria, P. & Hankin, C. | Non-deterministic games and program analysis: An application to security [BibTeX] |
1999 | Logic in Computer Science, 1999. Proceedings. 14th Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Maslov, A. N. | Multilevel stack automata [BibTeX] |
1976 | Problems of Information Transmission | article | |

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

Maslov, A. N. | The hierarchy of indexed languages of an arbitrary level [BibTeX] |
1974 | Soviet Math. Dokl. | article | |

BibTeX:
@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} } |
|||||

McCusker, G. | On the semantics of Idealized Algol without the bad-variable constructor [BibTeX] |
2003 | Nineteenth Conference on the Mathematical Foundations of Programming Semantics | inproceedings | |

BibTeX:
@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} } |
|||||

McCusker, G. | Games and Full Abstraction for a Functional Metalanguage with Recursive Types [BibTeX] |
1996 | School: Imperial College |
phdthesis | |

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

McCusker, G. | Games and Full Abstraction for FPC [BibTeX] |
1996 | Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, LICS 1996 | inproceedings | |

BibTeX:
@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} } |
|||||

McMillan, K. L. | Interpolation and SAT-Based Model Checking. [BibTeX] |
2003 | CAV | inproceedings | |

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

Meyer, A. | The Inherent Computational Complexity of Theories of Ordered Sets [BibTeX] |
1974 | Proc. Int'l. Cong. of Mathematicians | inproceedings | |

BibTeX:
@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} } |
|||||

Minsky, M. L. | Computation: finite and infinite machines [BibTeX] |
1967 | book | ||

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

de Miranda, J. G. | Structures generated by higher-order grammars and the safety constraint. [BibTeX] |
2006 | School: University of Oxford |
phdthesis | |

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

Murawski, A. | On program equivalence in languages with ground-type references [BibTeX] |
2003 | Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Murawski, A. S. | Games for complexity second-order call-by-name programs [BibTeX] |
2005 | Theoretical Computer Science | article | |

BibTeX:
@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} } |
|||||

Murawski, A. S. | About the undecidability of program equivalence in finitary languages with state | 2005 | ACM Trans. Comput. Logic | article | |

Abstract: We show how game semantics can be employed to prove that program equivalence in finitary Idealized Algol with active expressions is undecidable. We also investigate a notion of representability of languages by terms and show that finitary Idealized Algol terms of respectively second, third and higher orders define exactly regular, context-free and recursively enumerable languages. |
|||||

BibTeX:
@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} } |
|||||

Murawski, A. S. | About the undecidability of program equivalence in finitary languages with state | 2005 | ACM Trans. Comput. Logic | article | |

Abstract: We show how game semantics can be employed to prove that program equivalence in finitary Idealized Algol with active expressions is undecidable. We also investigate a notion of representability of languages by terms and show that finitary Idealized Algol terms of respectively second, third and higher orders define exactly regular, context-free and recursively enumerable languages. |
|||||

BibTeX:
@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} } |
|||||

Murawski, A. S. | On program equivalence in languages with ground-type references [BibTeX] |
2003 | misc | URL | |

BibTeX:
@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} } |
|||||

Murawski, A. S., Ong, C. L. & Walukiewicz, I. | Idealized Algol with Ground Recursion, and DPDA Equivalence. [BibTeX] |
2005 | ICALP | inproceedings | |

BibTeX:
@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} } |
|||||

Murawski, A. S. & Walukiewicz, I. | Third-Order Idealized Algol with Iteration Is Decidable. [BibTeX] |
2005 | FoSSaCS | inproceedings | URL |

BibTeX:
@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"} } |
|||||

N. Eén & N. Sörensson | An Extensible SAT-solver. [BibTeX] |
2003 | SAT | inproceedings | |

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

Nickau, H. | Hereditarily Sequential Functionals [BibTeX] |
1994 | Proc. Symp. Logical Foundations of Computer Science: Logic at St. Petersburg | inproceedings | |

BibTeX:
@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} } |
|||||

Ong, C. | On Model-Checking Trees Generated by Higher-Order Recursion Schemes [BibTeX] |
2006 | Logic in Computer Science, 2006 21st Annual IEEE Symposium on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Ong, C. L. | On model-checking trees generated by higher-order recursion schemes (Technical report) [BibTeX] |
2006 | unpublished | URL | |

BibTeX:
@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} } |
|||||

Ong, C. L. | On model-checking trees generated by higher-order recursion schemes [BibTeX] |
2006 | Proceedings of IEEE Symposium on Logic in Computer Science. | inproceedings | |

BibTeX:
@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} } |
|||||

Ong, C. L. | Safe Lambda Calculus: Some Questions [BibTeX] |
2005 | unpublished | ||

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

Ong, C. L. | An approach to deciding observational equivalence of Algol-like languages. [BibTeX] |
2004 | Ann. Pure Appl. Logic | article | |

BibTeX:
@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} } |
|||||

Ong, C. L. | Observational equivalence of third-order Idealized Algol is decidable [BibTeX] |
2002 | Proceedings of IEEE Symposium on Logic in Computer Science, 22-25 July 2002, Copenhagen Denmark | inproceedings | URL |

BibTeX:
@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} } |
|||||

Plotkin, G. D. | LCF Considered as a Programming Language. [BibTeX] |
1977 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Plotkin, G. D. | Call-by-name, call-by-value and the [lambda]-calculus | 1975 | Theoretical Computer Science | article | DOIURL |

Abstract: This paper examines the old question of the relationship between ISWIM and the [lambda]-calculus, using the distinction between call-by-value and call-by-name. It is held that the relationship should be mediated by a standardisation theorem. Since this leads to difficulties, a new [lambda]-calculus is introduced whose standardisation theorem gives a good correspondence with ISWIM as given by the SECD machine, but without the letrec feature. Next a call-by-name variant of ISWIM is introduced which is in an analogous correspondence withthe usual [lambda]-calculus. The relation between call-by-value and call-by-name is then studied by giving simulations of each language by the other and interpretations of each calculus in the other. These are obtained as another application of the continuation technique. Some emphasis is placed throughout on the notion of operational equality (or contextual equality). If terms can be proved equal in a calculus they are operationally equal in the corresponding language. Unfortunately, operational equality is not preserved by either of the simulations. |
|||||

BibTeX:
@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} } |
|||||

Podelski, A. & Rybalchenko, A. | Transition predicate abstraction and fair termination [BibTeX] |
2005 | POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Podelski, A. & Rybalchenko, A. | Transition Invariants [BibTeX] |
2004 | LICS '04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04) | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Princeton University | zChaff [BibTeX] |
misc | |||

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

Rea, N., Dahyot, R. & Kokaram, A. | Modeling high level structure in sports with motion driven HMMs [BibTeX] |
2004 | Acoustics, Speech, and Signal Processing, 2004. Proceedings. (ICASSP '04). IEEE International Conference on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Reynolds, J. C. | The Essence of ALGOL [BibTeX] |
1981 | Algorithmic Languages | incollection | |

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

Schubert, A. | The complexity of beta-reduction in low orders [BibTeX] |
Proceedings TLCA 2001 | article | ||

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

Schwichtenberg, H. | An upper bound for reduction sequences in the typed $-calculus [BibTeX] |
1991 | Archive for Mathematical Logic | article | |

BibTeX:
@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} } |
|||||

Schwichtenberg, H. | Definierbare Funktionen im Lambda-Kalkul mit Typen [BibTeX] |
1976 | Archiv Logik Grundlagenforsch | article | URL |

BibTeX:
@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} } |
|||||

Scott, D. S. | A type-theoretical alternative to ISWIM, CUCH, OWHY [BibTeX] |
1993 | Theor. Comput. Sci. | article | DOI |

BibTeX:
@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} } |
|||||

Scott, D. S. | A theory of computable function of higher type [BibTeX] |
1969 | unpublished | ||

BibTeX:
@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} } |
|||||

Sereni, D. | Simply typed $-calculus and SCT [BibTeX] |
2005 | unpublished | ||

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

Statman, R. | Intuitionistic propositional logic is polynomial-space complete [BibTeX] |
1979 | Theoretical Computer Science | article | URL |

BibTeX:
@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} } |
|||||

Statman, R. | The typed lambda -calculus is not elementary recursive [BibTeX] |
1979 | #j-THEOR-COMP-SCI# | article | |

BibTeX:
@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} } |
|||||

Stirling, C. | Deciding DPDA Equivalence Is Primitive Recursive [BibTeX] |
2002 | ICALP '02: Proceedings of the 29th International Colloquium on Automata, Languages and Programming | inproceedings | |

BibTeX:
@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} } |
|||||

Stockmeyer, L. J. & Meyer, A. R. | Word problems requiring exponential time(Preliminary Report) [BibTeX] |
1973 | STOC '73: Proceedings of the fifth annual ACM symposium on Theory of computing | article | DOI |

BibTeX:
@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} } |
|||||

Sun, J. & Zhang, Y. | A study on parallel semantics of constraint logic programs [BibTeX] |
2005 | Machine Learning and Cybernetics, 2005. Proceedings of 2005 International Conference on | inproceedings | DOI |

BibTeX:
@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} } |
|||||

Sénizergues, Gé. | L(A)=L(B)? decidability results from complete formal systems. [BibTeX] |
2001 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Tait, W. | Intensional Interpretations of Functionals of Finite Type I [BibTeX] |
1967 | J. Symb. Log. | article | |

BibTeX:
@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} } |
|||||

Thomas, W. | Languages, Automata, and Logic [BibTeX] |
1997 | misc | URL | |

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

Wikipedia | Wikipedia, the free encyclopedia. [BibTeX] |
2004 | misc | ||

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

Zaionc, M. | Lambda Representation of Operations Between Fifferent Term Algebras [BibTeX] |
1995 | CSL '94: Selected Papers from the 8th International Workshop on Computer Science Logic | article | |

BibTeX:
@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} } |
|||||

Zaionc, M. | Lambda-Definability on Free Algebras [BibTeX] |
1991 | Ann. Pure Appl. Logic | article | |

BibTeX:
@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} } |
|||||

Zaionc, M. | On the "lambda"-definable tree operations [BibTeX] |
1990 | Proceedings of the Conference on Algebraic Logic and Universal Algebra in Computer Science | article | |

BibTeX:
@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} } |
|||||

Zaionc, M. | On the "lambda"-definable tree operations [BibTeX] |
1988 | Algebraic Logic and Universal Algebra in Computer Science | inproceedings | |

BibTeX:
@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} } |
|||||

Zaionc, M. | Word Operation Definable in the Typed lambda-Calculus [BibTeX] |
1987 | Theor. Comput. Sci. | article | |

BibTeX:
@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} } |
|||||

Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings [BibTeX] |
2007 | TLCA | proceedings | ||

BibTeX:
@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} } |
|||||

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 [BibTeX] |
2005 | FoSSaCS | proceedings | ||

BibTeX:
@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} } |
|||||

Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings [BibTeX] |
2005 | ICALP | proceedings | ||

BibTeX:
@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} } |
|||||

Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings [BibTeX] |
2005 | SAS | proceedings | ||

BibTeX:
@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} } |
|||||

Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings [BibTeX] |
2005 | TLCA | proceedings | ||

BibTeX:
@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} } |
|||||

Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings [BibTeX] |
2003 | CAV | proceedings | ||

BibTeX:
@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, Ninth Annual IEEE Symposium on Logic in Computer Science, 4-7 July 1994, Paris, France [BibTeX] |
1994 | LICS | proceedings | ||

BibTeX:
@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} } |
|||||

Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings [BibTeX] |
1993 | TLCA | proceedings | ||

BibTeX:
@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} } |

Created by JabRef on 28/07/2008.