Stephen Cole Kleene

How to use this course

Stephen Cole Kleene was one of the founders of recursion theory, the mathematical study of what can and cannot be computed. As a graduate student of Alonzo Church he helped show that the λ-definable functions are exactly the general recursive ones. He then built the subject’s working machinery: the normal form theorem, partial recursive functions, the recursion theorem, the arithmetical and hyperarithmetical hierarchies and, with Emil Post, the theory of degrees. He gave intuitionistic logic a computational meaning through realizability. And in a report for the RAND Corporation in 1951 he invented regular expressions, now built into every text editor and programming language. His textbook Introduction to Metamathematics (1952) trained generations of logicians.

Each technical lesson opens with a paragraph for the general reader, then gives precise statements, proof sketches and exercises with folded solutions. We write \(\varphi_e\) for the \(e\)-th partial recursive function, \(\varphi_e(x)\!\downarrow\) when it is defined, \(\simeq\) for equality of partial values (both sides undefined, or both defined and equal), and \(W_e\) for the domain of \(\varphi_e\). Lessons 04 to 06 follow the work of 1936–1943; Lessons 07 and 08 the 1950s; Lesson 09 the intuitionistic work begun in 1945; Lesson 10 the automata theory of 1951.

Timeline

Hartford, Maine and Amherst, 1909–1930

Stephen Cole Kleene was born in Hartford, Connecticut, on 5 January 1909. His father, Gustav Adolph Kleene, the son of German immigrants, was professor of economics at Trinity College in Hartford. His mother, Alice Lena Cole, was a published poet and playwright. The family name is pronounced “clay-nee”.

Kleene grew up between Hartford and his paternal grandfather’s farm in Union, Maine, which he regarded as his real home. He returned to it nearly every summer of his life. From Maine came his lasting enthusiasms: mountain climbing, natural history, and the conservation of wild land. He became expert on mushrooms, and a variety of butterfly that he discovered was named after him.

Amherst

He studied at Amherst College in Massachusetts and graduated summa cum laude in 1930. In the autumn he began graduate work in mathematics at Princeton, then quickly becoming one of the leading mathematical centres in the world. From 1933 the new Institute for Advanced Study shared Fine Hall with the university’s mathematics department.

Princeton, 1930–1935

At Princeton Kleene became, with J. Barkley Rosser, one of Alonzo Church’s first doctoral students. Church was developing a new formal system for the foundations of logic, built entirely from functions written with his abstraction operator \(\lambda\). Kleene’s task was to develop the theory of the positive integers inside it.

The test case was the predecessor function, \(n\mapsto n-1\). Church himself doubted it could be defined with his numerals, which encode \(n\) as “apply a function \(n\) times”. Kleene found the trick: iterate on pairs, carrying the previous value along (Exercise 4.3 of the Church course). After that, function after function fell. His thesis, A Theory of Positive Integers in Formal Logic (1934, published 1935), showed that a very wide class of number-theoretic functions is λ-definable. The evidence it provided was one of the main reasons Church proposed, in 1935, that λ-definability captures exactly the effectively calculable functions.

The paradox and Gödel’s lectures

In 1934 Kurt Gödel lectured at the Institute for Advanced Study on his incompleteness theorems and on a new notion of general recursive function, suggested by Jacques Herbrand. Kleene and Rosser took the notes, which circulated widely and were later printed. In 1935 the two students proved that Church’s full logical system was inconsistent, as was the combinatory logic of Haskell Curry: a version of the Richard paradox could be derived in each. The Kleene–Rosser paradox ended Church’s logic, but its consistent core, the λ-calculus, survived.

Kleene then proved the theorem that tied the threads together. In “λ-definability and recursiveness” (1936) he showed that the λ-definable functions are exactly the general recursive functions of Herbrand and Gödel. Two independent definitions of computability coincided, and when Alan Turing’s machines were shown equivalent in 1937, the case for Church’s thesis was complete.

Madison, Princeton and the Navy, 1935–1946

In 1935 Kleene became an instructor in mathematics at the University of Wisconsin in Madison, the university he served, apart from interruptions, for the rest of his career. He was promoted to assistant professor in 1937. His papers of these years laid the foundations of recursion theory as a subject: the normal form theorem (1936, Lesson 04), partial recursive functions and the recursion theorem (1938, Lesson 05), and the arithmetical hierarchy (1943, Lesson 06). With Church he also studied effective notations for ordinal numbers, which led to the constructive ordinals of Lesson 08.

He spent 1939–40 at the Institute for Advanced Study in Princeton and 1941–42 as an associate professor at Amherst. In 1942 he married Nancy Elliott, daughter of an Amherst English professor; they had four children. That year he entered the US Naval Reserve as a lieutenant. He taught navigation at the Naval Reserve Midshipmen’s School in New York and then directed a project at the Naval Research Laboratory in Washington. In 1945, still in the Navy, he published his first paper on realizability (Lesson 09). He left the service in 1946 as a lieutenant commander and returned to Wisconsin as an associate professor.

General recursive functions and the normal form

For the general reader. In 1934 Gödel defined a class of functions computable by systems of equations, the general recursive functions. In 1936 Kleene gave them a much simpler description: start from a few basic functions, and allow composition, recursion and one new operation, “search for the least number such that…”. He then proved that every computable function needs only one search, applied to a single fixed, very simple relation. That relation, Kleene’s \(T\)-predicate, is the universal computer of recursion theory.

Primitive recursion and minimization

The primitive recursive functions on \(\mathbb N\) are the smallest class containing zero, successor \(x\mapsto x+1\) and the projections \((x_1,\dots,x_n)\mapsto x_i\), and closed under composition and primitive recursion:

Addition, multiplication, exponentiation, bounded sums and products, and the characteristic functions of “\(x\) is prime” and “\(y\) codes a valid computation” are primitive recursive. Not every computable function is: Wilhelm Ackermann’s function grows faster than any of them. Kleene added the μ-operator. For a partial function \(g\),

undefined if there is no such \(y\). The partial recursive functions are those obtained from the basic functions by composition, primitive recursion and μ. In 1936 Kleene worked with total functions and applied μ only when a witness always exists; the general recursive functions are the total partial recursive functions.

Proof idea. Code each derivation of a partial recursive function from the basic ones by a number \(e\). Code a complete computation, the finite tree of all intermediate values, by a number \(y\). The relation “\(y\) codes a correct computation of the function with index \(e\) on input \(\vec x\)” can be checked by bounded loops, so \(T_n\) is primitive recursive; \(U(y)\) reads the output off the root. Since computations are unique, the least \(y\) is the computation. ∎ Exactly one unbounded search is needed. Kleene originally coded systems of Herbrand–Gödel equations and their derivations, and the same argument works for Turing machines, λ-terms, or programs in any language.

The universal function

Write \(\varphi_e(\vec x)\simeq U(\mu y\,T_n(e,\vec x,y))\). Every partial recursive function appears in the list \(\varphi_0,\varphi_1,\dots\), and the function \((e,\vec x)\mapsto\varphi_e(\vec x)\) is itself partial recursive: a universal function, the mathematical form of a stored-program computer.

Partial functions and the recursion theorem

For the general reader. A program can be given its own text as data. Kleene proved in 1938 that, whatever transformation one applies to programs, some program behaves exactly like its own transformed version. This is the recursion theorem. It explains why programs that print their own code exist, why self-reference is unavoidable in any general computing system, and why almost no interesting question about what a program does can be decided automatically.

Partiality

In “On notation for ordinal numbers” (1938) Kleene made partial recursive functions the basic objects, rather than total ones. Without this step no universal function exists (Exercise 4.1). He also introduced the s-m-n theorem, which lets one fix some arguments of a program and compute an index for the result.

Proof. By s-m-n there is a total recursive \(d\) with \(\varphi_{d(u)}(y)\simeq\varphi_{\varphi_u(u)}(y)\) whenever \(\varphi_u(u)\!\downarrow\) (and \(\varphi_{d(u)}\) is nowhere defined otherwise). The composite \(f\circ d\) is total recursive; let \(v\) be an index of it. Then \(\varphi_v(v)=f(d(v))\) is defined, and with \(e=d(v)\),

For the second form, let \(f(x)=s(\hat\psi,x)\), where \(\hat\psi\) is an index of \(\psi\). ∎ The proof is the same diagonal construction as the fixed-point combinator in the λ-calculus, and the same trick that produces Gödel’s self-referential sentence.

The first recursion theorem and three-valued logic

Kleene also proved what he later called the first recursion theorem: every enumeration operator \(\Phi\) on partial functions, such as the right-hand side of a recursive definition, has a least fixed point, and that fixed point is partial recursive. It is the computational form of the order-theoretic fixed-point theorem that now bears his name, and the basis of the denotational semantics of programming languages. To reason about predicates that may be undefined, the same 1938 paper introduced a logic with a third value, “undefined”, in which a disjunction is true as soon as one disjunct is true even if the other is undefined. This strong Kleene logic is used today in philosophy of language and in the semantics of databases.

The arithmetical hierarchy

For the general reader. “Does this program halt?” asks whether some step of the computation is the last one: one search. “Does this program halt on every input?” asks for every input whether there is such a step: two nested searches, one of each kind. Kleene showed in 1943 that unsolvable problems form an infinite ladder, classified by the number of alternating “for all” and “there exists” needed to state them, and that each rung is genuinely harder than the one below.

Adjacent quantifiers of the same kind merge, by pairing, so only alternations count. Thus \(\Sigma_1\) sets are the recursively enumerable ones, the domains \(W_e\), and \(\Delta_1\) is the class of recursive sets.

Proof. For \(n=1\), \(S_1=\{(e,x):\exists y\,T_1(e,x,y)\}\) works by the normal form theorem. Higher levels follow by prefixing quantifiers to an enumeration of the level below. For (ii), let \(D=\{x:(x,x)\in S_n\}\). If \(D\) were \(\Pi_n\), its complement would be \(\Sigma_n\), equal to the section of \(S_n\) at some \(e\); then \(e\notin D\iff(e,e)\in S_n\iff e\in D\). ∎ For \(n=1\), \(D\) is the halting set \(K=\{x:\varphi_x(x)\!\downarrow\}\). Kleene also showed that \(\Delta_1\) is the recursive sets: if \(A\) and its complement are both r.e., search both enumerations in parallel.

Kleene’s hierarchy is the arithmetical analogue of the Borel hierarchy of descriptive set theory, a parallel he exploited fully in Lesson 08. Post showed in 1948 that \(A\) is \(\Sigma_{n+1}\) exactly when \(A\) is r.e. relative to the \(n\)-th jump of \(\emptyset\) (Lesson 07). In the same 1943 paper Kleene called Church’s proposal “Thesis I”; in Introduction to Metamathematics he named it Church’s thesis.

Degrees of unsolvability

For the general reader. If one had an oracle that answered the halting problem, which further problems could one solve? Problems can be compared by asking whether one becomes solvable with the other as an oracle. In 1954 Kleene and Emil Post began the systematic study of this ordering and found that it is far from a simple ladder: there are problems neither of which helps to solve the other, both strictly easier than the halting problem.

A set \(A\) is Turing reducible to \(B\), \(A\le_TB\), if the characteristic function of \(A\) is partial recursive relative to \(B\): computable by an algorithm that may ask finitely many questions “\(n\in B\)?”. Relativizing the normal form gives indices \(\varphi_e^B\). Sets with \(A\le_TB\le_TA\) have the same degree. The join \(A\oplus B=\{2n:n\in A\}\cup\{2n+1:n\in B\}\) gives the least upper bound of two degrees, so the degrees form an upper semilattice. The jump is \(A'=\{e:\varphi_e^A(e)\!\downarrow\}\), the halting problem relative to \(A\); \(\mathbf 0'\) is the degree of \(K\).

Proof of (ii). Build \(A\) and \(B\) as limits of finite binary strings \(\alpha_0\subseteq\alpha_1\subseteq\cdots\) and \(\beta_0\subseteq\beta_1\subseteq\cdots\), meeting the requirements \(R_{2e}:A\ne\varphi_e^B\) and \(R_{2e+1}:B\ne\varphi_e^A\) one at a time. To meet \(R_{2e}\) at stage \(s\): let \(n=|\alpha_s|\), a position where \(A\) is not yet decided. Ask whether some finite \(\beta\supseteq\beta_s\) makes \(\varphi_e^\beta(n)\) converge. If so, take the first such \(\beta\) found, set \(\beta_{s+1}=\beta\), and choose \(\alpha_{s+1}(n)\) different from the computed value. If not, \(\varphi_e^B(n)\) will diverge for any \(B\) extending \(\beta_s\), and the requirement is met automatically. The question asked is a \(\Sigma_1\) question, answerable by \(\emptyset'\), so the whole construction is computable from \(\emptyset'\). ∎

Post had asked in 1944 whether there is a recursively enumerable set strictly between \(\emptyset\) and \(K\). The Kleene–Post sets are computable from \(\emptyset'\) but not r.e. Post’s problem was solved in 1956–57, independently by Albert Muchnik and Richard Friedberg, with the priority method, a refinement of the Kleene–Post construction.

Constructive ordinals and hyperarithmetic sets

For the general reader. One can count past infinity with ordinals: \(\omega\), \(\omega+1\), \(\omega\cdot2\), \(\omega^2\), and so on. Which of these can be named by a finite program? Church and Kleene answered in 1936–38 with a system of notations, and Kleene used it to extend the arithmetical hierarchy into the transfinite. The result, the hyperarithmetic sets, turned out to be exactly the sets that can be defined both with and without a quantifier over all infinite sequences, a theorem that joined recursion theory to classical descriptive set theory.

Kleene’s \(\mathcal O\)

An ordinal is constructive (recursive) if it has a notation in \(\mathcal O\). The constructive ordinals form a countable initial segment of the ordinals; their supremum is the Church–Kleene ordinal \(\omega_1^{\mathrm{CK}}\). It is also the supremum of the order types of recursive well-orderings of \(\mathbb N\).

The hyperarithmetic hierarchy

Iterate the jump along notations: \(H_1=\emptyset\), \(H_{2^a}=(H_a)'\), and \(H_{3\cdot5^e}=\{\langle u,n\rangle:u\lt_{\mathcal O}3\cdot5^e,\ n\in H_u\}\). Spector proved in 1955 that the degree of \(H_a\) depends only on \(|a|\). A set is hyperarithmetic if it is recursive in some \(H_a\). The finite levels recover the arithmetical hierarchy, and \(H_{3\cdot5^e}\) for a notation of \(\omega\) computes every arithmetical set.

Let \(\Pi^1_1\) be the class of sets \(\{x:\forall f\in\mathbb N^{\mathbb N}\ \exists y\ R(x,\bar f(y))\}\) with \(R\) recursive and \(\bar f(y)\) a code for \((f(0),\dots,f(y-1))\); \(\Sigma^1_1\) uses \(\exists f\), and \(\Delta^1_1=\Sigma^1_1\cap\Pi^1_1\). These are the analytical sets, defined with quantifiers over functions.

Part (i) is the effective analogue of Mikhail Suslin’s theorem of 1917 that the Borel sets are exactly the sets that are both analytic and coanalytic, and it is called the Suslin–Kleene theorem. Its proof rests on representing \(\Pi^1_1\) sets by trees.

Every \(\Pi^1_1\) set has the form \(\{x:T_x\text{ has no infinite branch}\}\) for a recursive family of trees \(T_x\). By the Kleene–Brouwer criterion, \(x\in A\) iff a recursive linear ordering is a well-ordering, and well-orderings of recursive type are exactly those of type \(\lt\omega_1^{\mathrm{CK}}\), which links \(\Pi^1_1\) sets to \(\mathcal O\). Kleene’s students John Addison and Clifford Spector developed this theory, and Addison made the analogy with classical descriptive set theory systematic.

Realizability

For the general reader. For an intuitionist such as L. E. J. Brouwer, to assert “there exists a number with property P” is to promise a way of finding one, and to assert “A or B” is to promise a way of deciding which. Kleene made this precise in 1945: a statement is realized by a number coding a program that carries out the promises. Every theorem of intuitionistic arithmetic turns out to be realized, so its proofs contain algorithms. Realizability became a central method of constructive mathematics and of the extraction of programs from proofs.

Write \((e)_0,(e)_1\) for the components of a pair coded by \(e\). For closed formulas of arithmetic, Kleene defined “\(e\) realizes \(A\)”, written \(e\ \mathbf r\ A\), by induction on \(A\):

The proof, by induction on derivations, was carried out by Kleene’s first doctoral student, David Nelson, in his 1946 thesis. Two consequences: if \(\mathsf{HA}\vdash\forall x\,\exists y\,A(x,y)\) then there is a recursive \(f\) with \(A(n,f(n))\) true for every \(n\) (program extraction); and if \(\mathsf{HA}\vdash A\vee B\) for closed \(A,B\), then \(\mathsf{HA}\) proves \(A\) or proves \(B\) (Kleene later obtained this disjunction property by a variant, realizability combined with provability). Realizability also shows that \(\mathsf{HA}\) is consistent with the formal version of Church’s thesis, “every total function is recursive”, which is false classically under the intended reading but realizable.

Kleene developed realizability for analysis with functions as realizers in The Foundations of Intuitionistic Mathematics (1965), written with his student Richard Vesley. In 1982 Martin Hyland organized realizability into a topos, the effective topos, in which all functions from \(\mathbb N\) to \(\mathbb N\) are computable.

Regular events and finite automata

For the general reader. In 1943 Warren McCulloch and Walter Pitts modelled the brain as a network of on-off neurons. In the summer of 1951, at the RAND Corporation, Kleene asked exactly which patterns of input such a network, or any machine with finitely many internal states, can recognize. His answer was a short algebra of patterns built from three operations: “or”, “followed by”, and “repeated any number of times”. These are the regular expressions. Through Ken Thompson’s implementations in the QED and ed text editors from 1968 they became one of the most widely used pieces of mathematics in computing.

Regular expressions

Fix a finite alphabet \(\Sigma\). Languages are sets of finite strings. For languages \(L,M\) let \(L\cup M\) be the union, \(LM=\{uv:u\in L,\,v\in M\}\) the concatenation, and

the Kleene star, with \(\varepsilon\) the empty string. The regular languages are the smallest class containing \(\emptyset\), \(\{\varepsilon\}\) and each \(\{a\}\), \(a\in\Sigma\), closed under these three operations; a regular expression is a term describing how one is built. Kleene called them regular events, events being sets of input histories of a nerve net, and his original iteration operator was binary, \(E{*}F\); the unary star is the later convention.

A deterministic finite automaton is \(\mathcal A=(Q,\Sigma,\delta,q_0,F)\) with \(Q\) finite, \(\delta:Q\times\Sigma\to Q\), start state \(q_0\) and accepting set \(F\subseteq Q\). It accepts \(w\) if reading \(w\) from \(q_0\) ends in \(F\).

Automaton to expression (Kleene’s construction). Number the states \(1,\dots,m\). Let \(R^k_{ij}\) be the set of strings that lead from state \(i\) to state \(j\) passing through intermediate states only in \(\{1,\dots,k\}\). Then \(R^0_{ij}\) is a finite set of letters (plus \(\varepsilon\) if \(i=j\)), and

since a path through state \(k\) splits at its visits to \(k\). By induction each \(R^k_{ij}\) is regular, and the accepted language is \(\bigcup_{j\in F}R^m_{q_0j}\). The same recursion, with sets replaced by numbers and star by a suitable closure, computes shortest paths (Floyd–Warshall) and inverts matrices; it is an instance of an algebraic structure now called a Kleene algebra.

Expression to automaton. Build nondeterministic automata for the basic languages and combine them for union, concatenation and star by adding connecting transitions; then remove nondeterminism by the subset construction of Michael Rabin and Dana Scott (1959). Robert McNaughton and Hisao Yamada (1960) and Ken Thompson (1968) gave the constructions used in practice.

Take \(p\) the number of states of an automaton for \(L\): reading the first \(p\) letters visits \(p+1\) states, so one repeats, and the loop between the repeats can be traversed any number of times.

The Wisconsin school, 1946–1979

Back at Wisconsin, Kleene became professor in 1948 and Cyrus C. MacDuffee Professor of Mathematics in 1964. He spent 1950 in Amsterdam as a Guggenheim fellow, talking with the Dutch intuitionists around Brouwer and Arend Heyting, and spoke on recursive functions and intuitionistic mathematics at the International Congress of Mathematicians in Cambridge, Massachusetts, that year.

Introduction to Metamathematics (1952) was the first complete textbook of the new logic. It covered formal systems, Gödel’s theorems, recursive functions, Turing machines, Church’s thesis and intuitionism, all with full proofs, and it was translated into several languages. Two further books followed: The Foundations of Intuitionistic Mathematics with Vesley (1965) and the more elementary Mathematical Logic (1967). In 1959 he began a theory of computation on functionals of higher type, objects that take functions as arguments, which became a field of its own.

He supervised thirteen doctoral dissertations at Wisconsin. His students included David Nelson (1946), John Addison and Clifford Spector (both 1955), Richard Vesley (1962), Yiannis Moschovakis (1963), Joan Rand Moschovakis (1965), Robert Constable and Dick de Jongh (both 1968). Spector, who died young in 1961, proved the consistency of analysis by bar recursion; Yiannis Moschovakis became a leader of descriptive set theory; Constable founded the Nuprl proof system. Kleene was president of the Association for Symbolic Logic from 1956 to 1958, an editor of the Journal of Symbolic Logic, and in 1961 president of the International Union of the History and Philosophy of Science.

He served Wisconsin as chair of mathematics twice, as chair of the department of numerical analysis that became computer science, and from 1969 to 1974 as Dean of the College of Letters and Science, through the years of student protest against the Vietnam War, which on campus culminated in the bombing of Sterling Hall, home of the Army Mathematics Research Center, in August 1970. He was elected to the National Academy of Sciences in 1969.

The mountaineer

Kleene was a serious climber. In 1949 he set out with Saunders Mac Lane and a third companion to climb all the peaks of the Presidential Range in New Hampshire; on Mount Madison lightning struck and injured the companion, and Kleene went for help. He led the logic group’s picnic at Devil’s Lake near Madison, where logicians climbed the quartzite cliffs, a tradition continued as the Kleene Memorial Logic Picnic.

Last years, death and legacy, 1979–1994

Kleene retired in 1979 but continued to write, including historical accounts of the origins of recursive function theory and of the work of Gödel. His wife Nancy had died in 1970; he later married Jeanne Steinmetz, who survived him. He received the Leroy P. Steele Prize of the American Mathematical Society in 1983 and the National Medal of Science in 1990. He died of pneumonia in Madison on 25 January 1994, aged 85. In 1999 the mathematics library of the University of Wisconsin was named after him.

Legacy

• Recursion theory: the normal form theorem, partial recursive functions, the s-m-n and recursion theorems, the arithmetical and hyperarithmetical hierarchies and the theory of degrees remain the framework of the subject.
• Descriptive set theory: the effective hierarchies and the Suslin–Kleene theorem began the unification of recursion theory with classical descriptive set theory.
• Constructive mathematics: realizability is a basic tool of intuitionistic logic, type theory and program extraction from proofs.
• Computer science: regular expressions and Kleene’s theorem are the foundation of lexical analysis, text search and automata theory; Kleene algebras are used in program verification; his least fixed points underlie the semantics of recursive programs.
• Honours: the Kleene Award for the best student paper at the annual Symposium on Logic in Computer Science bears his name.

Sources and further reading

Biography

1. J. J. O’Connor and E. F. Robertson, Stephen Cole Kleene, MacTutor History of Mathematics.
2. Stephen Cole Kleene, Wikipedia.
3. S. Mac Lane, Stephen Cole Kleene 1909–1994, National Academy of Sciences, Biographical Memoirs 75 (1998).
4. Stephen Cole Kleene, Mathematics Genealogy Project.
5. S. C. Kleene, Origins of recursive function theory, Annals of the History of Computing 3 (1981) 52–67.
6. R. I. Soare, Computability and recursion, Bulletin of Symbolic Logic 2 (1996) 284–321.

Mathematics

1. S. C. Kleene, A theory of positive integers in formal logic, Amer. J. Math. 57 (1935) 153–173, 219–244.
2. S. C. Kleene and J. B. Rosser, The inconsistency of certain formal logics, Ann. of Math. 36 (1935) 630–636.
3. S. C. Kleene, General recursive functions of natural numbers, Math. Ann. 112 (1936) 727–742.
4. S. C. Kleene, λ-definability and recursiveness, Duke Math. J. 2 (1936) 340–353.
5. S. C. Kleene, On notation for ordinal numbers, J. Symbolic Logic 3 (1938) 150–155.
6. S. C. Kleene, Recursive predicates and quantifiers, Trans. Amer. Math. Soc. 53 (1943) 41–73.
7. S. C. Kleene, On the interpretation of intuitionistic number theory, J. Symbolic Logic 10 (1945) 109–124.
8. D. Nelson, Recursive functions and intuitionistic number theory, Trans. Amer. Math. Soc. 61 (1947) 307–368.
9. S. C. Kleene, Representation of events in nerve nets and finite automata, RAND RM-704, 1951; in C. E. Shannon and J. McCarthy (eds.), Automata Studies, Princeton, 1956, 3–41.
10. S. C. Kleene, Introduction to Metamathematics, North-Holland and Van Nostrand, 1952.
11. S. C. Kleene and E. L. Post, The upper semi-lattice of degrees of recursive unsolvability, Ann. of Math. 59 (1954) 379–407.
12. S. C. Kleene, Hierarchies of number-theoretic predicates, Bull. Amer. Math. Soc. 61 (1955) 193–213.
13. S. C. Kleene, Recursive functionals and quantifiers of finite types I, Trans. Amer. Math. Soc. 91 (1959) 1–52.
14. S. C. Kleene and R. E. Vesley, The Foundations of Intuitionistic Mathematics, North-Holland, 1965.
15. H. Rogers, Theory of Recursive Functions and Effective Computability, McGraw-Hill, 1967.
16. G. E. Sacks, Higher Recursion Theory, Springer, 1990.
17. J. van Oosten, Realizability: An Introduction to its Categorical Side, Elsevier, 2008.