Andrej Bauer 
selected papers and notes 
"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]
