Corrado Böhm was born on January 17th 1923 in Milan, Italy, and lived there until 1942, when he left Italy for Switzerland. At the time he was a student in Engineering.

He graduated in Electrical Engineering in 1946, at the University of Lausanne, in Switzerland, and shortly afterwards he became a research assistant at the ETH (the Swiss Federal Institute of Technology) in Zürich.

The beginning of Corrado’s activity in Computer Science can be traced back to 1947, when he was asked to collaborate in the performance evaluation of the computing machine Z4 of Konrad Zuse, the computer pioneer. The encounter with Zuse and his work was a crucial moment in the development of Corrado’s scientific ideas. His Ph.D. dissertation in Mathematics, which he submitted in 1951, was in fact a first bridge between the computer and the mathematics disciplines. In his thesis Corrado developed a language, a machine, and a translation met

hod for compiling that language on the machine. As remarked by D.E. Knuth in his paper “The early development of programming languages” [with L.T. Pardo, in: Metropolis, Howlett and Rota, eds., A History of Computing in the Twentieth Century, Annals of the History of Computing (Academic Press, New York, 1980) 197–268]: “Böhm’s dissertation was especially remarkable because he not only described a complete compiler, he also defined that compiler in its own language! And the language was interesting in itself, because every statement (including input statements, output statements and control statements) was a special case of an assignment statement.” This is in fact the first known example of what is now called a meta-circular compiler.  Corrado described his compiler four years before FORTRAN was defined and seven years before the definition of LISP! The dissertation was published as  [3]. His official thesis supervisor was Eduard Stiefel, but, as Corrado himself likes to recall, it was really Paul Bernays who stimulated his interest in Turing machines and universal computing machines.

Another pioneering result achieved by Corrado Böhm in those years was that of proposing a computing machine for symbolic evaluation. This machine is described in detail, together with the input and output peripherals, in a patent filed in 1952 (Brevetto industriale italiano no. 43.3186).

In 1951 Corrado moved back to Italy. After a period of work at Olivetti-Ivrea in 1953, he became a permanent researcher at the IAC-CNR (Istituto per le Applicazioni del Calcolo – Consiglio Nazionale delle Ricerche) in Rome. At that time the Institute, under the direction of the mathematician Mauro Picone, was involved in a project with Ferranti in Manchester, England, aimed at developing the first (partially Italian) computer, the FINAC (Ferranti-Istituto Nazionale Applicazioni Calcolo). Again Corrado was in charge of the performance evaluation of the computer. To this end he went to Manchester in order to feed FINAC with a system of 63 algebraic equations! Among other contributions to the FINAC, Corrado designed a system called INTINT (INTerpretation-INTegration) for handling vectors.

From 1952 to 1959 Corrado’s main activity at IAC concerned differential and integral calculus and its numerical applications.

The fifties were particularly important years for Corrado also from a personal point of view. In 1950 he married Eva Romanin Jacur, a fascinating lady from Padova and a talented painter. In 1955 their first son Michele was born; in 1958 came their second son Emanuele and in 1960 their daughter Ariela. They are now, respectively, a computer artist, a scholar in oceanography and a sculptor.

It was about this time that Corrado’s work at IAC started moving towards Theoretical Computer Science.

From 1960 to 1968 Corrado continued working at IAC and also lectured in Computer Science at the University of Rome. Giorgio Ausiello, Daniel Bovet, Giuseppe Jacopini, Alfonso Miola, and Marisa Venturni Zilli, among others, were his students at the time. During these years Corrado worked on the theory of Turing machines [14,23]. His aim was to apply the theory of Turing machines and recursive functions to programming Von Neumann machines. In 1966 he proved, together with his student Giuseppe Jacopini a seminal result in this area, nowadays known as the Böhm-Jacopini theorem [16]. As E.W. Dijkstra puts in a letter to Communications of ACM [11 (3) (1968) 147-148], “[they show] the (logical) superfluousness of the GOTO statement”. The Böhm-Jacopini theorem is considered the theoretical basis of structured programming, the well-known programming style developed and advocated by many researchers in the seventies. This methodology opened a new and more disciplined view of programming and today “programming”  really means “programming in a structured way”. More than 200 citations to [16] appear in the literature on “structured programming” of those years. As just one example we mention the book Structured Programming by O.J. Dahl and E.W. Dijkstra and C.A.R. Hoare (Academic Press, New York, 1972).

In the sixties Corrado was one of the first to investigate a new research field in Computer Science: the λ-calculus. As early as 1963 a dissertation dealing with applications of -calculus to Computer Science was written under his supervision by Marisa Venturini Zilli for her degree in Mathematics; the precise content of this thesis was the representation within λ-calculus of data types used in Iverson’s language APL. Together with his friend Wolf Gross, Corrado introduced the CUCH, a functional programming language based on Curry’s theory of combinators and Church’s λ-calculus; see [15, 17]. (CUCH is in fact an acronym obtained from the names of these two logicians.) These papers were the starting point of a fruitful research programme, whose aim was to study the properties of functional programming languages by analyzing the properties of paradigmatic abstract languages based on λ-calculus.

In 1968 Corrado obtained a seminal result in the theory of λ-calculus, which is nowadays known as Böhm’s theorem [22]. What he proved was that two terms of λ-calculus having syntactically different normal forms with respect to β-η-reduction cannot be consistently equated. In fact, there always exists a context that discriminates between them. This result was proved in order to show soundness of a programming language based on λ-calculus, like CUCH, where the β- and η-reduction rules are used as evaluation rules and normal forms are taken as results of computations. Apart from this motivating application, this theorem has been shown to have many important and surprising other consequences, for example the maximality of the theory induced by the standard D λ-model λdefined by D. Scott [Continuous lattices, in Lawvere, ed., Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics, Vol. 274 (Springer, Berlin, 1972) 97-136]. The importance of Böhm’s theorem lies not only in the result itself, but also in the technique used for proving it, which has been termed the Böhm-out technique in Barendregt’s encyclopaedic book on λ-calculus; see [The Lambda Calculus, its Syntax and Semantics (North-Holland, Amsterdam, 1984)]. The proof of this theorem also suggested to Henk Barendregt a very useful representation of λ-terms as trees, which he called Böhm trees. Böhm trees have been widely used in the literature and they play an important role in the syntactic and semantic analysis of λ-calculus.

In 1964 Corrado was one of the promoters of the Working Group 2.2 (Formal Description of Programming Concepts) of IFIP (the International Federation of Information Processing) together with De Bakker, Landin, Scott, Strachey and others. The aim of this group was “to explicate programming concepts through the development, examination and comparison of various formal models of these concepts”. The activities of this group have been extremely influential on later Theoretical Computer Science. For instance, early ideas in formal languages for describing the semantics of programming languages, such as denotational semantics, arose and were thoroughly debated during the meetings of this group. Corrado’s inclusion in this group was an indication of his international standing and of the widely acknowledged relevance of his work. In this period Corrado was established as the leading Italian researcher in the field of Computer Science and one of the most important theoretical computer scientists in the rest of the world.

In 1968 he was appointed as full professor in Computer Science. After a short time spent at the Mathematics Department of the University of Modena, he moved to the University of Turin, where he was appointed head of the project of organizing an undergraduate course in Computer Science in the Faculty of Sciences. (This was only the second project of this kind in Italy, after the one in Pisa, which started in 1969.) Corrado pursued this project with great enthusiasm, notwithstanding the many difficulties due to the lack of resources made available to him by the University. The only computer facility consisted of one IBM 360/44 for the whole of the faculty of Sciences, and the “Computer Science Institute” was located in one single room, which Corrado had to share with all his collaborators. In 1970-71 Corrado met Mariangiola Dezani-Ciancaglini, Mario Coppo, Ines Margaria, Simona Ronchi Della Rocca, and Maddalena Zacchi; all of them had only recently graduated and had been awarded fellowships to do research under Corrado’s supervision. Corrado spent four years in Turin and during this time he was very successful in organizing the Institute and the undergraduate programme. He also succeeded in obtaining improved logistical conditions for his Institute and in convincing the University to devote more financial resources to increasing the computer facilities. He also taught courses on “Systems for Data Processing” and “Formal Languages and Compilers”.

Despite the large amount of time he spent in teaching and organizing during those years, Corrado also did very fruitful research work, establishing in particular a research group in Theoretical Computer Science at the University of Turin. In the field of λ-calculus, he designed an abstract machine for the call-by-name evaluation of terms, which is interesting for its automatic treatment of α-conversion; see [26-28]. Moreover he applied the Böhming-out technique to finding solutions for equations between λ-terms; see [34]. In another direction, he started investigating the problem of coding, with integers, families of “information structures”,  as he called them, i.e. datatypes, with the aim of saving memory space. Together with Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca he developed coding methods based both on generating functions and on questionnaires [24, 25, 29-33].

In 1974 he moved back to the University of Rome, where he taught “Programming Techniques”. In the same year he organized in Rome an International Conference on Lambda Calculus. This meeting was one of the first to concentrate on this topic and the list of the many open problems collected during the meeting deeply influenced future research; see [36]. Some of these were solved only many years later and some are still open. The paper [37], presented at this conference by Corrado (in collaboration with Mariangiola Dezani-Ciancaglini), together with its successor [39], can be considered as the starting point of the intersection type discipline which was developed by the Turin research group during the following years.

In 1975 Corrado also became a member of the Editorial Board of  Theoretical Computer Science, a new journal edited by North-Holland, which rapidly became one of the most prestigious European journals on the subject.

It was in the mid-seventies that Corrado started to develop those ideas which have appeared to be central to his studies in recent years. Namely, that normalization is the paradigmatic algorithm and, hence, that the only interesting computations are those that can be coded as strongly normalizing terms. Only programs definable using strictly gauged iterative combinators are amenable to a significant analysis while recursive programs obtained using a brute force application of the fixed point combinator are often not very significant. In this view, Corrado’s research can be roughly classified into two mainstreams.

First, representation of data structures, and of programs manipulating them, as -terms; representation which are then suitable for writing iterative programs instead of recursive ones.

Second, solutions of equations between λ-terms and the closely linked separability of problems.

Obviously this classification does not give a full idea of the extent of Corrado’s output in these years (approximately two/thirds of his papers have been published between 1980 and 2000); we will mention only some of the most important results.

In [41, 43] Combinatory Logic is presented as an extension of elementary number theory.

In [46] the notion of minimal form, i.e. of a -term which reduces to itself, was introduced and characterized. This paper was written in collaboration with Silvio Micali, a student of Corrado at the time, who has been honoured with the Gödel award in 1993.

In a series of papers [50, 53, 54, 57, 59, 62], Corrado showed the possibility of replacing recursion by iteration, at the price of changing, in a suitable way, the representation of data structures. The advantage of doing this is that one obtains surely terminating programs.

His research activity on the representation of data structures inside λ-calculus started with [45]. A very important result in this direction was obtained by Corrado in collaboration with Alessandro Berarducci, a student of his, and was presented in [52]. It is the automatic translation from the definition of a free algebra, given via the generators, to the representation of the elements of the algebra by means of terms of Girard’s system F (Interprétation Fonctionnelle et élimination des coupures dans l’arithmetique d’ordre supérieur, Thèse de Doctorat d’État, Université de Paris VII, 1972). This representation result can be considered as a cornerstone in the design of functional programming languages.

In collaboration with Adolfo Piperno and Enrico Tronci, he studied the problem of solving equations between λ-terms and of characterizing invertibility properties of λ-terms; see [56, 58, 60, 64].

The paper [68] written in collaboration with Benedetto Intrigila proposes the “ant-lion” paradigm. This is a general method for finding strongly normalizable solutions to fixed point equations.

The paper [67] connects his old research on the CUCH machine to his new views on data representations. A very user-friendly functional programming language suitable for writing polymorphic programs is the outcome of this work.

In 1988 a new IFIP working group WG 2.8 (Functional Programming) was established: Corrado was among the promoters. The aim of this WG is “to study the design, implementation and the use of (applicative) functional languages”.

From 1989 to 1991, Corrado was the coordinator of an EEC-funded “ESPRIT” working group, WG 3230, on “Common Foundations of Functional and Logic Programming”. The level of scientific output of this group was very high and the EEC has financed a successor with Corrado as a coordinator, being WG 7232  “Gentzen” (1992-1994).

In 2001 Corrado won the EATCS Award. This prize is awarded in recognition of a distinguished career in theoretical computer science.

Corrado is today active and hard-working as he has always been in his life. He is still greatly in love with Science. He is ready, at any moment, to speculate on general scientific problems as well as to discuss highly technical questions. And this he is ready to do with great enthusiasm with young students as well as senior researchers.

Corrado’s scientific curiosity urges him to seek new fields, like biology and anthropology, but without losing sight of topics studied earlier. We are confident that his future research activity will continue to contribute to the development of Computer Science.

Selected bibliography

[1] Scomposizioni di un sistema di sostituzioni lineari in un sistema di transfert, Rend. Mat. Pura Appl. (5) 12 (1,2) (1953) 76-78.

[2] Nuovi criteri di esistenza di soluzioni periodiche di una nota equazione differenziale non lineare. Ann. Mat. Pura Appl. (4) 35 (1954) 343-353.

[3] Calculatrices digitales. Di déchiffrage des formules logico-mathématiques par la machine même dans la conception du programme, Ann. Mat. Pura Appl. (4) 37 (1954) 1-51.

[4] Sulla programmazione mediante formule, Proc. 4 Sessione Giornate della Scienza, La Ricerca Scietifica 24 (1954) 1008-1014.

[5] Perfezionamento di un processo iterativo atto alla divisione automatica, La Ricerca Scientifica 25 (7) (1955) 2077-2080.

[6] Sulla valutazione automatica della precisione di calcolo, in: Proc. Simposio su L’Automazione del Calcolo e il Progresso dell’Analisi Matematica, SIPS (1956) 121-130.

[7] INTINT programmazione indiretta per calcolatrici elettroniche, Manuali per le Applicazioni Tecniche del Calcolo, Vol. 3, Cremonese, Roma (1958).

[8] Sulla minimizzazione di una funzione del prodotto di enti non commutativi, Rend. Accad. Naz. Lincei (classe Sci. Fis. Mat. Nat.) (8) 23 (6) (1958) 386-389.

[9] Sur le circle de rayon minimum ayant distance nulle d’un ensemble de circles coplanaires, in: Proc. Colloque sur des Questions d’Analyse Numérique, INAC-CNR Vol. 540, Roma (1959).

[10] (with L. Calamia) Ricerca di una misura di efficienza negli algoritmi grafici, in: Proc. Convegno Nazionale di Logica, Levrotto e Bella, Torino (1961) 137-151.

[11] (with G. Jacopini) Nuove tecniche di programmazione semplificanti la costruzione di macchine universali di Turing, Rend. Accad. Naz. Lincei (classe Sci. Fis. Mat. Nat.) (8) 32 (1962).

[12] Macchine a indirizzi, dotate di un numero minimo di istruzioni, Rend. Accad. Naz. Lincei (classe Sci. Fis. Mat. Nat.) (1962).

[13] (with A. Santolini) A quasi-decision algorithm for the equivalence of two matrices, Internat. Comput. Center Bull. (3) 1 1964.

[14] On a family of Turing machines and related programming language, Internat. Comput. Center Bull. (3) 3 1964.

[15] (with W. Gross) Introduction to the CUCH, in: E.R. Caianiello, ed., Automata Theory (Academic Press, London 1966) 35-65.

[16] (with G. Jacopini) Flow diagrams, Turing machines and languages with only two formation rules, Comm. ACM (9) 5 (1966) 366-371.

[17] The CUCH as a formal and description language, in: T.B.Steel, Jr., ed., Formal Languages Description Languages for Computer Programming (North-Holland, Amsterdam, 1966) 179-197.

[18] Basi Matematiche della programmazione, Calcolo (2) 2 (1965) 1-17.

[19] (with G. Ausiello) Applicazioni del linguaggio CUCH alla programmazione di macchine analogiche sequenziali, in: Proc. IX Convegno-Mostra dell’Automazione e Strumentazione, Fast, Milano (1966) 329-358.

[20] A self-instructional approach to computer language, INAC (8) 670 (1966).

[21] (with H. Moncayo Lopez and G. Ausiello) Costruzione di un interprete CINAC per il linguaggio LISP (ROMALISP I), INAC (10) 695 (1967) 49-73.

[22] Alcune proprietà delle forme normali nel calcolo, INAC 696 (1968).

[23] A three-tape, three-state, three-symbol universal Turing machine, INAC 698 (1968).

[24] (with S. Ronchi Della Rocca) Numbering methods of finite sets and multisets through trees, in: Proc. ACM Internat. Comp. Symp., Venice (1972).

[25] Strutture informative e loro trasformazioni, in: Proc. III Seminario sul Trattamento Automatico delle Informazioni, Firenze (1972).

[26] (with M. Dezani) A CUCH-machine: the automatic treatment of bound variables, Internat. J. Comput. Inform. Sci. (1) 2 (1972) 171-191.

[27] (with M. Dezani-Ciancaglini) Can syntax be ignored during translation?, in: M. Nivat, ed., Automata, Languages and Programming (North-Holland, Amsterdam, 1972) 197-207.

[28] (with M. Dezani) Notes on “A CUCH-machine: the automatic treatment of bound variables”, Internat. J. Comput. Inform. Sci. (2) 2 (1973) 157-160.

[29] (with M. Dezani-Ciancaglini) Listing the functional digraph structures, in: A. Günther, B. Levrat and H. Lipps, eds., Proc. Internat. Comp. Symp. (North-Holland, Amsterdam, 1973) 33-39.

[30] (with M. Dezani-Ciancaglini) Data structures and their transformations, Control Cybernet. (3) 3/4 (1974) 5-19.

[31] (with M. Dezani-Ciancaglini and S. Ronchi Della Rocca) Questionario per strutture informative, in: Proc. Convegno di Informatica Teorica, Ed. Tec. Sci., Pisa (1974) 153-174.

[32] (with M. Dezani-Ciancaglini) A data structure formalization through generating functions, Calcolo 1 (1974) 47-66.

[33] (with M. Dezani-Ciancaglini and S. Ronchi Della Rocca) Listing of information structures defined by fixed-point operators, in: B. Robinet, ed., Proc. Colloque sur la Programmation, Lecture Notes in Computer Science, Vol. 19 (Springer, Berlin, 1974) 266-279.

[34] (with M. Dezani-Ciancaglini) Combinatorial problems, combinator equations and normal forms, in: J. Loeckx, ed., Proc. II Coll. Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 14 (Springer, Berlin, 1974) 185-199.

[35] (with M. Dezani-Ciancaglini) To what extent can or must computations be parallelized, in: E.R. Caianiello, ed., New Concepts and Technologies in Parallel Information Processing (Noordhoff, Leyden, 1975) 137-154.

[36] (with M. Dezani-Ciancaglini) terms as total or partial functions on normal forms, in: C. Böhm, ed., Proc. Lambda-Calculus and Computer Science Theory, Lecture Notes in Computer Science, Vol. 37 (Springer, Berlin, 1975) 96-121.

[37] (with M. Dezani-Ciancaglini) terms as total or partial functions on normal forms, in: C. Böhm, ed., Proc. Lambda-Calculus and Computer Science Theory, Lecture Notes in Computer Science, Vol. 37 (Springer, Berlin, 1975) 96-121.

[38] (with M. Dezani-Ciancaglini) Attribute Semantics, Some uses of generating functions in theoretical computer science. Riv. Inform. (7) 1 (1977) 85-94, 95-107.

[39] (with M. Coppo and M. Dezani-Ciancaglini) Termination test inside -calculus, in: A. Salomaa and M. Steinby, eds., Proc. IV Coll. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 52 (Springer, Berlin, 1977) 95-110.

[40] (with G. Sontacchi) On the existence of cycles of given length in integer sequences like xn+1=xn/2 if xn even, and xn+1=3xn+1 otherwise, Rend. Accad. Naz. Lincei (classe Sci. Fis. Mat. Nat.) (64) 3 (6) (1978) 260-264.

[41] Un modèle arithmétique des termes de la logique combinatoire, in: B. Robinet, ed., Proc.  Sixième Ecole de Printemps d’Informatique Theorique – Lambda Calcul et Semantique Formelle des Langages de Programmation, LITP and ENSTA (1979)97-108.

[42] (with M. Dezani-Ciancaglini, P. Peretti and S. Ronchi Della Rocca) A discrimination Algorithm inside  --calculus, Theoret. Comput. Sci. 8 (1979) 271-291.

[43] Logic and Computers – combinatory logic as extension of elementary number theory, in: E. Agazzi, ed., Modern Logic – A Survey (Reidel, Dordrecht, 1980) 297-309.

[44] (with A. Machì and G. Sontacchi) Complexity bounds for equivalences and isomorphism of Latin squares, Inform. Process. Lett. 10 (4,5) (1980) 231-233.

[45] An abstract approach to (hereditary) finite sequences of combinator, in: J.P. Seldin and J.R. Hindley, eds., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, London, 1980) 231-242.

[46] (with S. Micali) Minimal forms in lambda-calculus computations, Symbolic logic 45 (1) (1980) 165-171.

[47] (with G. Sontacchi) Riduzioni ed equivalenze di giochi di tipo Nim, in: Proc. Convegno Nazionale sui Giochi Creativi,  Siena (1981) 160-166.

[48] Combinatory foundation of functional programming, in: Proc. ACM Symp. On LISP and Functional Programming, Pittsburgh (1982) 29-36.

[49] Vers l’exploitation du parallelisme en programmation fonctionelle (abstract), in: Proc. 5me rencontre RCP Algorithmique, Limoges (1982).

[50] (with D. Kozen) Eliminating recursion over acyclic data structures in functional programs (abstract), in: Proc. 4th Internat. Workshop on the Semantics of Programming Languages, EATCS Bull. 20 (1983) 205.

[51] (with M. Dezani-Ciancaglini) Combinatory logic as monoids (extended abstract) in: Proc. Atti del Congresso Logica e Filosofia della Scienza, CLUEB, Bologna (1986) 169-178.

[52] (with A. Berarducci) Automatic synthesis of typed lambda-programs on term algebras, Theoret. Comput. Sci. 39 (1985) 135-154.

[53] Reducing recursion to iteration by algebraic extension, in: B. Robinet and R. Wilhelm, eds., Proc. ESOP 86 – European Symp. On Programming, Lecture Notes in Computer Science, Vol. 213 (Springer, Berlin, 1986) 111-118.

[54] Sviluppo di una teoria uniforme per la programmazione di funzioni totali ricorsive su algebre, in: R. Ferro and A. Zanardo, eds., Proc. Logica ed Informatica: da Incidenti di Confine ad un’Alleanza di Interesse, CLEUP, Padova (1987) 349-357.

[55] (with E. Tronci) X-separability and left-invertibility in λ-calculus (extended abstract), in: Proc. Temi e Prospettive della Logica e della Filosofia della Scienza Contemporanea, CLUEB (1), Bologna (XXXX) 23-28.

[56] (with E. Tronci) X-separability and left-invertibility in λ-calculus, in: Proc. Symp. on Logic and Computer Science (IEEE Computer Soc. Press, Silver Spring, MD, 1987) 320-328.

[57] Reducing recursion to iteration by means of pairs and N-tuples (invited lecture), in: M. Boscarol, L. Carlucci Aiello and G. Levi, eds., Proc. Foundations of Logic and Functional Programming, Lecture Notes in Computer Science, Vol. 306 (Springer, Berlin, 1988) 58-66.

[58] (with A. Piperno) Characterizing X-separability and one-side invertibility in λ-β-Ω-calculus in: Proc. Symp. on Logic and Computer Science (IEEE Computer Soc. Press, Silver Spring, MD, 1988) 91-101.

[59] Functional programming and combinatory algebras (invited lecture), in: M.P. Chytil, L. Janiga and V. Koubek, eds., Pric. Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 324 (Springer, Berlin, 1988) 14-26.

[60] (with A. Piperno) Surjectivity for finite sets of combinators by weak reduction, in: E. Börger, H. Kleine Bühning and M.M. Richter, eds., Proc. 1st Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 326 (Springer, Berlin, 1988) 27-43.

[61] (with A. Piperno and E. Tronci) Solving equations in λ-calculus, in: A. Ferro, C. Bonotto, S. Valentini and A. Zanardo eds., Proc. Logic Coll. ’88 (North-Holland, Amsterdam, 1989) 139-160.

[62] Subduing self-application (invited paper), in G. Ausiello, M. Dezani-Ciancaglini and S. Ronchi Della Rocca, eds., Proc. 16th Coll. on Automata, Languages and Programming, Lecture Notes in Computer Science, (Springer, Berlin, 1989) 108-122.

[63] (with M. Dezani-Ciancaglini) Combinatory logic as monoids, Fund. Inform. 12 (1989) 525-540.

[64] (with E. Tronci) About systems of equations, X-separability and left-invertibility in the λ-calculus, Inform. And Comput. 90 (1990) 1-31.

[65] (with B. Intrigila) Multisets and polynomials: an algebraic approach to functional programming, Rend. Mat. (7) 10 (1990) 867-898.

[66] (with A. Berarducci) A self-interpreter of λ-calculus having normal form (invited lecture), in: Proc. Computer Science Logic 92, Lecture Notes in Computer Science, (Springer, Berlin, 1992), 85-99.

[67] (with A. Piperno and S. Guerrini) Lambda-Definition of Function(al)s by Normal Forms, in: Proc. ESOP 94, Lecture Notes in Computer Science, (Springer, Berlin, 1994), 135-149.

[68] (with B. Intrigila) The Ant-Lion Paradigm for Strong Normalization, Inform. And Comput. 114 (1994) 30-49.

[69] Theoretical Computer Science and Software Science: The Past, the Present and the Future (Position Paper). in: Proc. TAPSOFT 97, Lecture Notes in Computer Science, (Springer, Berlin, 1997), 3-5.

[70] Fixed Point Equations Inside the Algebra of Normal Forms. Fundam. Inform. 37(4) (1999) 329-342.

[71] (with A. Berarducci) General Recursion on Second Order Term Algebras, in: Proc. RTA 01, Lecture Notes in Computer Science, (Springer, Berlin, 2001),  15-30.