In this thesis we present two applications of sheaf semantics. The first is to give constructive proof of Newton-Puiseux theorem. The second is to show the independence of Markov's principle from type theory. In the ...

The extensive use of computers in mathematics and engineering has led to an increased demand for reliability in the implementation of algorithms in computer algebra systems. One way to increase the reliability is to formally ...