1. K. Aehlig & F. Joachimski (2002): A note on Böhm's theorem. Available at
  2. H.P. Barendregt (1984): The Lambda calculus: its syntax and semantics. North-Holland.
  3. C. Böhm (1968): Alcune proprietà delle forme βη-normali nel λK-calcolo.. Pubblicazioni dell'IAC 696.
  4. C. Böhm, M. Dezani-Ciancaglini, P. Peretti & S. Ronchi Della Rocca (1979): A discrimination algorithm inside lambda-beta-calculus. Theoretical Computer Science 8, pp. 265–292, doi:10.1016/0304-3975(79)90014-8.
  5. C. Böhm & W. Gross (1966): Introduction to the CUCH. In: E. Caianiello: Automata Theory. Academic Press, London, UK, pp. 35–65.
  6. C. Böhm, A. Piperno & S. Guerrini (1994): Lambda-Definition of Function(al)s by Normal Forms. In: D. Sannella: ESOP, Lecture Notes in Computer Science 788. Springer-Verlag, Berlin, Germany, pp. 135–149, doi:10.1007/3-540-57880-3_9.
  7. A. Carraro, T. Ehrhard & A. Salibra (2012): The Stack calculus. Submitted to LSFA12.
  8. R. David & W. Py (2001): λμ-Calculus and Böhm's Theorem. J. Symb. Log. 66(1), pp. 407–413, doi:10.2307/2694930.
  9. M. Dezani-Ciancaglini, S. Guerrini & A. Piperno (2009): Böhm's Theorem, pp. 1–15. World Scientific Pub. Co. Inc.. Available at
  10. M. Dezani-Ciancaglini, U. De' Liguoro & A. Piperno (1996): Filter Models for Conjunctive-disjunctive λ-calculi. Theoretical Computer Science 170(1-2), pp. 83–128, doi:10.1016/S0304-3975(96)00235-6.
  11. M. Dezani-Ciancaglini, J. Tiuryn & P. Urzyczyn (1999): Discrimination by parallel observers: the algorithm. Information and computation 150(2), pp. 153–186, doi:10.1006/inco.1998.2773.
  12. M. Felleisen (1990): On the expressive power of programming languages. In: ESOP. LNCS, pp. 134–151, doi:10.1007/3-540-52592-0_60.
  13. T. Griffin (1990): A Formulae-as-Types Notion of Control. In: POPL, pp. 47–58, doi:10.1145/96709.96714.
  14. C. Hankin (1995): Lambda Calculi: a guide for computer scientists. Oxford University Press.
  15. W.A. Howard (1980): The formulas-as-types notion of construction. In: J.R. Hindley & J.P. Seldin: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490.
  16. G.P. Huet (1993): An Analysis of Böhm's Theorem. Theor. Comput. Sci. 121(1&2), pp. 145–167, doi:10.1016/0304-3975(93)90087-A.
  17. J.M.E. Hyland (1976): A syntactic characterization of the equality in some models of the λ-calculus. J. London Math. Soc. 2(12), pp. 361–370, doi:10.1112/jlms/s2-12.3.361.
  18. S. Katsumata & K. Nakazawa (2012): Extensional models of untyped λμ-calculus. In: CL& C, doi:10.4204/EPTCS.97.3.
  19. G. Manzonetto & M. Pagani (2011): Böhm's theorem for resource lambda calculus through Taylor expansion. In: TLCA, pp. 153–168, doi:10.1007/978-3-642-21691-6_14.
  20. M. Parigot (1991): Free Deduction: An Analysis of ''Computations'' in Classical Logic. In: RCLP, pp. 361–380, doi:10.1007/3-540-55460-2_27.
  21. D. Prawitz (1965): Natural Deduction - a proof theoretical study. Almqvist & Wiksell, Stokholm.
  22. D. Sangiorgi (1994): The lazy lambda calculus in a concurrency scenario. Information and computation 111(1), pp. 120–153, doi:10.1006/inco.1994.1042.
  23. A. Saurin (2005): Separation with streams in the Λμ-calculus. In: LICS, pp. 356–365, doi:10.1109/LICS.2005.48.
  24. A. Saurin (2010): Standardization and Böhm Trees for Λμ-calculus. In: FLOPS, pp. 134–149, doi:10.1007/978-3-642-12251-4_11.
  25. A. Saurin (2010): Typing streams in the Λμ-calulus. ACM Trans. Comput. Log. 11(4), doi:10.1145/1805950.1805958.
  26. J.P. Seldin & J. Hindley (1986): Introduction to combinators and λ-calculus. Cambridge University Press.
  27. T. Streicher & B. Reus (1998): Classical logic, continuation semantics and abstract machines. J. Funct. Program. 6(8), pp. 543–572, doi:10.1017/S0956796898003141.
  28. C.P. Wadsworth (1976): The relation between computational and denotational properties for Scott's D_-models of the λ-calculus. SIAM Journal on Computing 5(3), pp. 488–521, doi:10.1137/0205036.

Comments and questions to:
For website issues: