H.P. Barendregt (1984):
The Lambda calculus: its syntax and semantics.
North-Holland.
C. Böhm (1968):
Alcune proprietà delle forme βη-normali nel λK-calcolo..
Pubblicazioni dell'IAC 696.
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.
C. Böhm & W. Gross (1966):
Introduction to the CUCH.
In: E. Caianiello: Automata Theory.
Academic Press,
London, UK,
pp. 35–65.
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.
A. Carraro, T. Ehrhard & A. Salibra (2012):
The Stack calculus.
Submitted to LSFA12.
R. David & W. Py (2001):
λμ-Calculus and Böhm's Theorem.
J. Symb. Log. 66(1),
pp. 407–413,
doi:10.2307/2694930.
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.
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.
M. Felleisen (1990):
On the expressive power of programming languages.
In: ESOP.
LNCS,
pp. 134–151,
doi:10.1007/3-540-52592-0_60.
T. Griffin (1990):
A Formulae-as-Types Notion of Control.
In: POPL,
pp. 47–58,
doi:10.1145/96709.96714.
C. Hankin (1995):
Lambda Calculi: a guide for computer scientists.
Oxford University Press.
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.
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.
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.
S. Katsumata & K. Nakazawa (2012):
Extensional models of untyped λμ-calculus.
In: CL& C,
doi:10.4204/EPTCS.97.3.
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.
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.
D. Prawitz (1965):
Natural Deduction - a proof theoretical study.
Almqvist & Wiksell,
Stokholm.
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.
A. Saurin (2005):
Separation with streams in the Λμ-calculus.
In: LICS,
pp. 356–365,
doi:10.1109/LICS.2005.48.
A. Saurin (2010):
Standardization and Böhm Trees for Λμ-calculus.
In: FLOPS,
pp. 134–149,
doi:10.1007/978-3-642-12251-4_11.
A. Saurin (2010):
Typing streams in the Λμ-calulus.
ACM Trans. Comput. Log. 11(4),
doi:10.1145/1805950.1805958.
J.P. Seldin & J. Hindley (1986):
Introduction to combinators and λ-calculus.
Cambridge University Press.
T. Streicher & B. Reus (1998):
Classical logic, continuation semantics and abstract machines.
J. Funct. Program. 6(8),
pp. 543–572,
doi:10.1017/S0956796898003141.
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.
eptcs@eptcs.org