The Universities of Stockholm and Uppsala

D. Normann, E. Palmgren and Stoltenberg-Hansen finished a study of hyperfinite type structures as models for dependent types.

E. Palmgren spent January - June 1997 in Göteborg. Together with Th. Couqand a method for extracting constructive content from classical proofs involving the axiom of choice was obtained. The method uses sheaves over countably complete boolean algebras.

Anton Setzer is a proof theoretist who has joined the group in Uppsala in April 1997. He is working on proof theory of Martin-Löf's type theory. He has introduced a new way of representing the proof theoretical ordinal of Martin-Löf's type theory, interpreted Kripke-Platek set theory into type theory, and is currently working together with P. Dybjer on a rigorous formulation of inductive recursive definitions. He has implemented a preliminary version of it in Half. Further, he has together with T. Coquand and P. Hancock (Edinburgh) worked on easier well-ordering proofs for versions of type theory without the W-type and carried out well-ordering proofs in Half.

V. Stoltenberg-Hansen, together with J. Blanck and J.V. Tucker (Swansea), has worked on the representability of topological algebras and higher type objects over topological algebras using domain theory.

Publications 1997 (relevant to TYPES)

• J. Blanck. Domain representability of metric spaces, Annals of Pure and Applied Logic 83 (1997), 225-247.
• E. Palmgren. A sheaf-theoretic foundation for nonstandard analysis. Annals of Pure and Applied Logic 85(1997), 69 - 86.
• E. Palmgren. Constructive sheaf semantics. Mathematical Logic Quarterly 43(1997), 321 - 327.
• E. Palmgren and V. Stoltenberg-Hansen. A logical presentation of the continuous functionals, Journal of Symbolic Logic 62(1997), 1021 - 1034.
• A. Setzer. Inductive Definitions with Decidable Prime Formulas, in van Dalen, D. and Bezem, M. (Eds.), Computer Science Logic, Lecture Notes in Computer Science, vol. 1258, 1997, pp. 414 - 430.
• A. Setzer. Translating set theoretical proofs into type theoretical programs,in Gottlob, G. and Leitsch, A. and Mundici, D. (Eds.), Computational Logic and Proof Theory, vol. 1289, 1997, pp. 278 - 289.
• I. Sigstam and V. Stoltenberg-Hansen. Representability of locally compact regular spaces by domains and formal spaces, Theoretical Computer Science 179 (1997), 319-331.

Preprints and submitted papers 1997

• P. Clote and A. Setzer. On PHP, st-connectivity, and odd charged graphs, to appear in: P. Beame and S. Buss (eds.), Proof Complexity and Feasible Arithmetics.
• Th. Coquand and E. Palmgren. Intuitionistic choice and classical logic. Dept. Mathematics, Chalmers University of Technology and Göteborg University, Preprint 1997:08.
• D. Normann, E. Palmgren and V. Stoltenberg-Hansen. Hyperfinite type structures. Dept. Mathematics, Uppsala University, Preprint 1997:10.
• A. Setzer. Well-ordering proofs for Martin-Löf Type Theory, to appear in Annals of Pure and Applied Logic.
• A. Setzer. An Introduction to Well-ordering Proofs in Martin-Löf's Type Theory, submitted.