Introduction
	A. NEW DIRECTIONS	1

L	The ultra-intuitionistic criticism and the antitraditional program for foundations of mathematics A. S. Yessenin- Volpin . . . Computable analysis and differential equations G. Aberth .
m.	Mathematics as a numerical language E. Bishop On the notion of randomness P. Martin-Löf
V.	Abstract quantification theory R. M. Smullyan 79
	B. TRADITIONAL INTUITIONISM	93

VI.	Recent progress in intuitionistic analysis A. Heyting ~ . . 95
	VII. A theory of constructions equivalent to arithmetic N. D. Goodman	101
	   Church’s thesis: a kind of reducibility axiom for constructive
	   mathematics G. Kreisel ~~	121
	   Formal systems of intuitionistic analysis The theory of species
	   J. Myhill	151
	   Projections of lawless sequences D. van Dalen and A. S. Troelstra	163
	   On subjective mathematical assertions B. van Rootselaar . .	187
	XII. A palatable substitute for Kripke’s schema R. E. Vesley . .	197

C.	CLASSICAL INTERPRETATIONS OF INTUITIONISM . .

A characterization of the intuitionistic propositional calculus
	D. H. J. de Jongh	211
Intuitionistic model theory and the Cohen independence proofs
	M. Fitting	219

Prof. Yessenin-Volpin was invited to give the opening address, and submitted the paper herein printed as l. However he was unfortunately unable to attend, and Prof. Heyting read the paper VI as an opening address.
Concluding address.
vi

XV.	An abstract notion of realizability for which intuitionistic predicate calculus is complete H. Läuchli
XVI.	Extending the topological interpretation to intuitionistic analysis D. Scott

D.	PROOF THEORY OF INTUITIONISM

Some results for intuitionistic logic with second order quantification rules D. Prawitz
On cut elimination in intuitionistic systems of analysis B. Scarpel-
	lini	271

E.	PROOF-THEORETIC ORDINALS

Hereditarily replete functionals over the ordinals S. Feferman .
XX.	Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis S. Feferman . . Brouwer’s bar theorem and a system of ordinal notations
H.	Gerber
XXII.	Regular ordinals and normal forms D. Isles
Formalization of the theory of ordinal diagrams of infinite order
A.Kino
On the relationship between Takeuti’s ordinal diagrams 0(n) and
	Schütte’s system of ordinal notations	H. Levitz .	. . 377

F.	PROOF THEORY

On the original Gentzen consistency proof for number theory
P.	Bernays t
XXVI.	Herbrand-style consistency proofs B. Dreben and J. Denton . . XXVII. Iterated inductive definitions and -AC H. Friedman . . .
Assignment of ordinals to terms for primitive recursive functionals of finite type W. A. Howard
On a number theoretic choice schema and its relation to induction Ch. Parsons
Applications of the cut elimination theorem to some subsystems of classical analysis W. W. Tait
XXXI.	Principles of proof and ordinals implicit in given concepts
	G. Kreisel	489

Bernays was unfortunately unable to attend, and so his paper XXV was read by Howard