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 >

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

**Files in This Item:**

File | Description | Size | Format | |
---|---|---|---|---|

gupea_2077_48250_1.pdf | Dissertation | 648Kb | Adobe PDF | View/Open |

gupea_2077_48250_2.pdf | spiklad | 63Kb | Adobe 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 |