Alpha-Structural Recursion and Induction

1. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)

   MATH  Google Scholar 

2. Cheney, J.: Nominal Logic Programming. PhD thesis, Cornell University (August 2004)

   Google Scholar 

3. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)

   Article  MATH  MathSciNet  Google Scholar 

4. de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math. 34, 381–392 (1972)

   Google Scholar 

5. Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS 1999, pp. 193–202. IEEE Computer Society Press, Los Alamitos (1999)

   Google Scholar 

6. Gabbay, M.J.: A Theory of Inductive Definitions with α-Equivalence: Semantics, Implementation, Programming Language. PhD thesis, University of Cambridge (2000)

   Google Scholar 

7. Gabbay, M.J.: FM-HOL, a higher-order theory of names. In: Kamareddine, F. (ed.) Workshop on Thirty Five years of Automath, Informal Proceedings, April 2002, Heriot-Watt University, Edinburgh (2002)

   Google Scholar 

8. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)

   Article  MATH  Google Scholar 

9. Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 173–191. Springer, Heidelberg (1996)

   Google Scholar 

10. Griffin, T.G.: Notational definition — a formal account. In: Proc. LICS 1988, pp. 372–383. IEEE Computer Society Press, Los Alamitos (1988)

    Google Scholar 

11. Gunter, C.A.: Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge (1992)

    MATH  Google Scholar 

12. Honsell, F., Miculan, M., Scagnetto, I.: An axiomatic approach to metareasoning on nominal algebras in HOAS. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 963–978. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

13. Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

14. Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 241–256. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

15. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. PLDI 1988, pp. 199–208. ACM Press, New York (1988)

    Google Scholar 

16. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)

    Article  MATH  MathSciNet  Google Scholar 

17. Plotkin, G.D.: An illative theory of relations. In: Cooper, R., Mukai, K., Perry, J. (eds.) Situation Theory and its Applications. CSLI Lecture Notes, vol. 1, 22, pp. 133–146. Stanford University (1990)

    Google Scholar 

18. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004)

    Google Scholar 

19. Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    Google Scholar 

20. Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science (2005) (To appear)

    Google Scholar 

21. Stoughton, A.: Substitution revisited. Theoretical Computer Science 59, 317–325 (1988)

    Article  MATH  MathSciNet  Google Scholar 

22. Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323, 473–497 (2004)

    Article  MATH  MathSciNet  Google Scholar 

23. Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Proc. CADE-20. LNCS. Springer, Heidelberg (2005)

    Google Scholar 

Download references