Andrej Bauer 
selected papers and notes 
"Two Constructive EmbeddingExtension Theorems
with Applications to Continuity Principles
and to BanachMazur Computability
", with Alex Simpson 
December 19, 2003 We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X, in such a way that every sequentially continuous function from Cantor space to Z extends to a sequentially continuous function from X to R. The second asserts an analogous property for Baire space relative to any inhabited locally noncompact CSM. Both results rely on having careful constructive formulations of the concepts involved. [postscript letter] [postscript A4] [PDF letter] [PDF A4]

"Propositions as [Types]", with Steven Awodey, technical report 
June 11, 2001 Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family. [postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF] [PDF A4] [DVI]

"A Relationship between Equilogical Spaces and Type Two Effectivity" 
April 10, 2001 In this paper I compare two well studied approaches to topological semanticsthe domaintheoretic approach, exemplified by the category of countably based equilogical spaces, wEqu, and Type Two Effectivity, exemplified by the category of Baire space representations, Rep(B). These two categories are both locally cartesian closed extensions of countably based T_{0}spaces. A natural question to ask is how they are related. [postscript] [gzip postscript] [PDF]

"Sheaf Toposes for Realizability", with Steven Awodey, preprint 
April 10, 2001 We compare realizability models over partial combinatory algebras by embedding them into sheaf toposes. We then use the machinery of Grothendieck toposes and geometric morphisms to study the relationship between realizability models over different partial combinatory algebras. This research is part of the Logic of Types and Computation project at Carnegie Mellon University under the direction of Dana Scott. [postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF]

"Continuous Functionals of Dependent Types and Equilogical
Spaces", with Lars Birkedal 
May 18, 2000 We show that dependent sums and dependent products of continuous parametrizations on domains with dense, codense, and natural totalities agree with dependent sums and dependent products in equilogical spaces, and thus also in the realizability topos RT(P(N)). [postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF]

"Mixed multibasic and hypergeometric Gospertype algorithms", with Marko Petkovsek 
August, 1997 Gosper's summation algorithm finds a hypergeometric closed form of an indefinite sum of hypergeometric terms, if such a closed form exists. We extend the algorithm to the case when the terms are simultaneously hypergeometric and multibasic hypergeometric. We also provide algorithms for finding polunomial as well as hypergeometric solutions to recurrences in the mixed case. We do not require the based to be transcedental, butonly that q_{1}^{k1} . . . q_{m}^{km} != 1 unless k_{1} = ... = k_{m} = 0. Finally, we generalize the concept of greatest factorial factorization to the mixed hypergeometric case. [postscript] [gzip postscript]

"Analytica  An Experiment in Combining
Theorem Proving and Symbolic Computation", with Edmund Clarke and Xudong Zhao 
August, 1997 Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to deduce correctness of certain simplification steps that would otherwise not be performed. We describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several nontrivial theorems. In this paper, we show how it can prove a series of lemmas that lead to Bernstein approximation theorem. [postscript] [gzip postscript]
