GUPEA >
IT Faculty / IT-fakulteten >
Department of Computer Science and Engineering / Institutionen för data- och informationsteknik >
Doctoral Theses / Doktorsavhandlingar Institutionen för data- och informationsteknik >

Sheaf Semantics in Constructive Algebra and Type Theory


Please use this identifier to cite or link to this item: http://hdl.handle.net/2077/48250

Files in This Item:

File Description SizeFormat
gupea_2077_48250_1.pdfDissertation648KbAdobe PDF
View/Open
gupea_2077_48250_2.pdfspiklad63KbAdobe PDF
View/Open
Title: Sheaf Semantics in Constructive Algebra and Type Theory
Authors: Mannaa, Bassel
E-mail: bassel.mannaa@gmail.com
Issue Date: 6-Oct-2016
University: Göteborgs universitet. IT-fakulteten
Institution: Department of Computer Science and Engineering ; Institutionen för data- och informationsteknik
Parts of work: Mannaa, B. and Coquand, T. [2013], ‘Dynamic newton-puiseux theo- rem’, J. Logic & Analysis 5.

Mannaa, B. and Coquand, T. [2014], A sheaf model of the algebraic closure, in P. Oliva, ed., ‘Proceedings Fifth International Workshop on Classical Logic and Computation, Vienna, Austria, July 13, 2014’, Vol. 164 of Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, pp. 18–32.

Coquand, T. and Mannaa, B. [2016], The independence of markov’s principle in type theory, in ‘1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal’, pp. 17:1–17:18.
Date of Defence: 2016-10-28
Disputation: 10:00 EDIT building, Chalmers, room EA
Degree: Doctor of Philosophy
Publication type: Doctoral thesis
Series/Report no.: 135D
Keywords: Newton–Puiseux theorem
Algebraic curve
Sheaf model
Dynamic evaluation
Type theory
Markov’s Principle
Forcing
Abstract: 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 first part we study Newton-Puiseux algorithm from a constructive point of view. This is the algorithm used for computing the Puiseux expansions of a plane algebraic curve defined by an affine equation over an algebraically closed field. The termination of this algorithm is usuall... more
ISBN: 978-91-628-9985-1 (Print)
978-91-628-9986-8 (PDF)
URI: http://hdl.handle.net/2077/48250
Appears in Collections:Doctoral Theses from University of Gothenburg / Doktorsavhandlingar från Göteborgs universitet
Doctoral Theses / Doktorsavhandlingar Institutionen för data- och informationsteknik

 

 

© Göteborgs universitet 2011