Semantics of HOT Languages
2009–10

Principal lecturer: Prof Andrew Pitts
Taken by: MPhil ACS

• Syllabus.
  
• Reading material.
  • The first part of the course will be based on

    A. M. Pitts, Operational Semantics and Program Equivalence. In: G. Barthe, P. Dybjer and J. Saraiva (Eds), Applied Semantics. Lecture Notes in Computer Science, Tutorial, Volume 2395 (Springer-Verlag, 2002), pages 378-412. [pdf © 2002 Springer-Verlag]

  • The second part of the course follows sections 1-3 of

    A. M. Pitts, Relational Properties of Domains, Information and Computation 127(1996) 66--90. [pdf]

    See also section 5 of

    S. Abramsky and A. Jung, Domain Theory In: Handbook of Logic in Computer Science, Vol. III, Clarendon Press, 1994, pages 1-168. [pdf]

• Slides
  • lecture 1: [colour] [greyscale, 2-up]
  • lecture 2: [colour] [greyscale, 2-up]
  • lecture 3: [colour] [greyscale, 2-up]
  • lecture 4: [colour] [greyscale, 2-up]
  • lecture 5: [colour] [greyscale, 2-up]
  • lecture 6: [colour] [greyscale, 2-up]
  • lecture 7: [colour] [greyscale, 2-up]
  • lecture 8: [colour] [greyscale, 2-up]
  • lecture 9: [colour] [greyscale, 2-up]
  • lecture 10: [colour] [greyscale, 2-up]
  • lecture 11: [colour] [greyscale, 2-up]
  • lecture 12: [colour] [greyscale, 2-up]
  • lecture 13: [colour] [greyscale, 2-up]
  • lecture 14: [colour] [greyscale, 2-up]
  • lecture 15: [colour] [greyscale, 2-up]
• Exam briefing and exercises (pdf).
• References.
  • S. Abramsky and G. McCusker, Game Semantics. In H. Schwichtenberg and U. Berger, editors, Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School. Pages 1-56. Springer-Verlag. 1999.
  • L. Birkedal and R. W. Harper, Constructing interpretations of recursives types in an operational setting, Information and Computation, 155:3-63, 1999.
  • K. Crary and R. Harper, Syntactic Logical Relations for Polymorphic and Recursive Types. In In L. Cardelli, M. Fiore and G. Winskel (eds), Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, Electronic Notes in Theoretical Computer Science, Volume 172 (Elsevier, 2007).
  • D. Dreyer, A. Ahmed, and L. Birkedal, Logical Step-Indexed Logical Relations, preprint, January 2010.
  • I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287-327, 1991.
  • A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names, Logical Methods in Computer Science, Vol. 4 (1:4) 2008, pp. 1-33.
  • A. M. Pitts and I. D. B. Stark, Operational Reasoning for Functions with Local State. In A.D. Gordon and A. M. Pitts (Eds), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute (Cambridge University Press, 1998), pp 227-273.
  • E. Sumii, A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References. In Proceedings of 18th EACSL Annual Conference on Computer Science Logic, Coimbra, Portugal, September 7-11, 2009 (Lecture Notes in Computer Science, Springer-Verlag, Germany, vol. 5771), pp. 455-469.
  • N. Yoshida and K. Honda and M. Berger, Local State in Hoare Logic for Imperative Higher-Order Functions. In Proc. Tenth International Conference on Foundations of Software Science and Computation Structures (FoSSACS 2007), Braga, Portugal 2007 (Lecture Notes in Computer Science, Springer-Verlag, Germany, vol. 4423), pp. 361-377.