Towards Ludics Programming: Interactive Proof Search

1. Girard, J.Y.: Locus solum. Mathematical Structures in Computer Science 11(3) (2001)

   Google Scholar 

2. Howard, W.A.: The formulae-as-type notion of construction, 1969. In: Seldin, Hindley (eds.) To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, New York (1980)

   Google Scholar 

3. Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51 (1991)

   Google Scholar 

4. Andreoli, J.M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3) (1992)

   Google Scholar 

5. Girard, J.Y.: Linear logic. Theoretical Computer Science 50 (1987)

   Google Scholar 

6. Naish, L.: Negation and Control in Prolog. LNCS, vol. 238. Springer, Heidelberg (1986)

   MATH  Google Scholar 

7. Naish, L.: Pruning in logic programming. Technical Report 95/16, Department of Computer Science, University of Melbourne, Australia (1995)

   Google Scholar 

8. Miller, D.: Sequent calculus and the specification of computation. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic. Nato ASI Series, vol. 165. Springer, Heidelberg (1999)

   Google Scholar 

9. Griffin, T.: A formulae-as-types notion of control. In: POPL 1990 (1990)

   Google Scholar 

10. Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

11. Faggian, C., Hyland, M.: Designs, disputes and strategies. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, p. 442. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

12. Abramsky, S., Jagadeesan, R.: Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59(2) (1994)

    Google Scholar 

13. Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF. Information and Computation 163 (2000)

    Google Scholar 

14. van Emden, M.H.: Quantitative deduction and its fixpoint theory. Journal of Logic Programming 3(1) (1986)

    Google Scholar 

15. Cosmo, R.D., Loddo, J.V., Nicolet, S.: A game semantics foundation for logic programming. In: PLILP/ALP (1998)

    Google Scholar 

16. Loddo, J.V., Cosmo, R.D.: Playing logic programs with the alpha-beta algorithm. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol. 1955. Springer, Heidelberg (2000)

    Google Scholar 

17. Loddo, J.V.: Généralisation des Jeux Combinatoires et Applications aux Langages Logiques. Ph.D thesis, Université Paris VII (2002)

    Google Scholar 

18. Pym, D., Ritter, E.: Reductive Logic and Proof-search: proof theory, semantics, and control, vol. 45. Oxford Logic Guides, Oxford (2004)

    Book  MATH  Google Scholar 

19. Pym, D., Ritter, E.: A games semantics for reductive logic and proof-search. In: Ghica, D., McCusker, G. (eds.) GaLoP 2005 (2005)

    Google Scholar 

20. Miller, D., Saurin, A.: A game semantics for proof search: Preliminary results. In: Proceedings of MFPS 2005. ENTCS, vol. 155 (2006)

    Google Scholar 

21. Delande, O., Miller, D.: A neutral approach to proof and refutation in MALL. In: Pfenning, F. (ed.) LICS 2008. IEEE Computer Society Press, Los Alamitos (2008)

    Google Scholar 

22. Galanaki, C., Rondogiannis, P., Wadge, W.W.: An infinite-game semantics for well-founded negation in logic programming. Annals of Pure and Applied Logic 151(2) (2008)

    Google Scholar 

23. Laurent, O.: Étude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (2002)

    Google Scholar 

24. Faggian, C.: Travelling on designs. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471. Springer, Heidelberg (2002)

    Google Scholar 

25. Fleury, M.R., Quatrini, M.: First order in ludics. Mathematical Structures in Computer Science 14(2) (2004)

    Google Scholar 

Download references