Skip to main content
SpringerLink
Log in

The Anatomy of Innocence

  • Conference paper
  • First Online:
Computer Science Logic (CSL 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2142))

Included in the following conference series:

Abstract

We reveal a symmetric structure in the ho/n games model of innocent strategies, introducing rigid strategies, a concept dual to bracketed strategies. We prove a direct definability theorem of general innocent strategies with respect to a simply typed language of extended Böhm trees, which gives an operational meaning to rigidity in call-by-name. A corresponding factorization of innocent strategies into rigid ones with some form of conditional as an oracle is constructed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In Proceedings, Thirteenth Annual IEEE Symposium on Logic in Computer Science, pages 334–344, 1998.

    Google Scholar 

  2. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In P. W. O’Hearn and R. D. Tennent, editors, Algol-like languages. Birkhaüser, 1997.

    Google Scholar 

  3. Vincent Danos and Russell Harmer. Probabilistic games semantics. In Proceedings of the 15 th Symposium on Logic in Computer Science, Santa Barbara, 2000. IEEE.

    Google Scholar 

  4. Vincent Danos, Hugo Herbelin, and Laurent Regnier. Games semantics and abstract machines. In Proceedings of the 11 th Symposium on Logic in Computer Science, pages 394–405, New Brunswick, 1996. IEEE.

    Google Scholar 

  5. Hugo Herbelin. Games and weak head reduction for classical PCF. In ?, editor, Proceedings of TLCA’97, number 1210 in Lecture Notes in Computer Science, pages ?-?, ?, 1997. Springer Verlag.

    Google Scholar 

  6. R. S. Harmer and G. A. McCusker. A fully abstract game semantics for finite nondeterminism. In Proceedings, Fourteenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.

    Google Scholar 

  7. J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. To appear in Information and Computation, 200?, 1994.

    Google Scholar 

  8. J. Laird. Full abstraction for functional languages with control. In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1997.

    Google Scholar 

  9. Olivier Laurent. Polarized proof nets and λμ-calculus. Submitted to Theoretical Computer Science, 1999.

    Google Scholar 

  10. P. B. Levy. Game semantics as continuation passing (extended abstract). unpublished, 1998.

    Google Scholar 

  11. Guy McCusker. Games and full abstraction for FPC. In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 174–183. IEEE Computer Society Press, 1996.

    Google Scholar 

  12. Guy McCusker. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. Distinguished Dissertations in Computer Science. Springer-Verlag, 1998.

    Google Scholar 

  13. P. Malacaria and C. Hankin. Non-deterministic games and program analysis: An application to security. In Proceedings, Fourteenth Annual IEEE Symposium on Logic in Computer Science IEEE Computer Society Press, 1999.

    Google Scholar 

  14. Hanno Nickau. Hereditarily sequential functionals. In Proceedings, Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  15. Peter Selinger. Control categories and duality: on the categorical semantics of the λμ-calculus. To appear, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Equipe Preuves, Programmes, Systèmes, Université Paris, 2 place Jussieu, 75251, Paris Cedex 05, France

    Vincent Danos

  2. School of Cognitive and Computing Sciences, University of Sussex, Brighton, BN1 9QH, UK

    Russell Harmer

Authors
  1. Vincent Danos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Russell Harmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LSV (Ecole Normale Supérieure de Cachan and CNRS), 61, Avenue du Président Wilson, 94230, Cachan, France

    Laurent Fribourg

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Danos, V., Harmer, R. (2001). The Anatomy of Innocence. In: Fribourg, L. (eds) Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, vol 2142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44802-0_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-44802-0_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42554-0

  • Online ISBN: 978-3-540-44802-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation