Game Semantics and Normalization by Evaluation

1. Abel, A.: Normalization by Evaluation: Dependent Types and Impredicativity. Institut für Informatik, Ludwig-Maximilians-Universität München, Habilitation thesis (May 2013)

   Google Scholar 

2. Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-Löf type theory with one universe. In: 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIII. Electronic Notes in Theoretical Computer Science, pp. 17–40. Elsevier (2007)

   Google Scholar 

3. Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)

   Article  MATH  MathSciNet  Google Scholar 

4. Aehlig, K., Joachimski, F.: Operational aspects of untyped normalisation by evaluation. Mathematical Structures in Computer Science 14(4) (2004)

   Google Scholar 

5. Amadio, R., Curien, P.-L.: Domains and lambda-calculi, vol. 46. Cambridge University Press (1998)

   Google Scholar 

6. Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λ-calculus. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pp. 203–211 (July 1991)

   Google Scholar 

7. Cartmell, J.: Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic 32, 209–243 (1986)

   Article  MATH  MathSciNet  Google Scholar 

8. Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science 24(5) (2013)

   Google Scholar 

9. Clairambault, P., Murawski, A.S.: Böhm trees as higher-order recursive schemes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, Guwahati, India, December 12-14, pp. 91–102 (2013)

   Google Scholar 

10. Curien, P.-L.: Abstract Böhm trees. Mathematical Structures in Computer Science 8(6), 559–591 (1998)

    Article  MATH  MathSciNet  Google Scholar 

11. Curien, P.-L.: Notes on game semantics. From the authors web page (2006)

    Google Scholar 

12. Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 120–134. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

13. Dybjer, P.: Program testing and the meaning explanations of intuitionistic type theory. In: Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, pp. 215–241 (2012)

    Google Scholar 

14. Dybjer, P., Kuperberg, D.: Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Logic 163(2), 122–131 (2012)

    Article  MATH  MathSciNet  Google Scholar 

15. Filinski, A., Rohde, H.K.: Denotational aspects of untyped normalization by evaluation. Theor. Inf. and App. 39(3), 423–453 (2005)

    Article  MATH  MathSciNet  Google Scholar 

16. Harmer, R., Hyland, M., Melliès, P.-A.: Categorical combinators for innocent strategies. In: 22nd IEEE Symposium on Logic in Computer Science, Wroclaw, Poland, Proceedings, pp. 379–388. IEEE Computer Society (2007)

    Google Scholar 

17. Hyland, J.M.E., Luke Ong, C.-H.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)

    Article  MATH  Google Scholar 

18. McCusker, G.: Games and full abstraction for FPC. Inf. Comput. 160(1-2), 1–61 (2000)

    Article  MATH  MathSciNet  Google Scholar 

19. Pitts, A.M.: A co-induction principle for recursively defined domains. Theor. Comput. Sci. 124(2), 195–219 (1994)

    Article  MATH  MathSciNet  Google Scholar 

20. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977)

    Article  MathSciNet  Google Scholar 

21. Plotkin, G.D.: Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Dept. of Computer Science, Univ. of Edinburgh (1981)

    Google Scholar 

Download references