19 citations · 50 across the 7 of their papers we have counts for
7 papers
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning ab…
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Bassel Mannaa, Rasmus Ejlers Møgelberg
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning ab…
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
Stack Semantics of Type Theory
Thierry Coquand, Bassel Mannaa, Fabian Ruch
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As…
The Independence of Markov's Principle in Type Theory
Thierry Coquand, Bassel Mannaa
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov…
A Sheaf Model of the Algebraic Closure
Bassel Mannaa, Thierry Coquand
In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure o…
Dynamic Newton-Puiseux Theorem
Bassel Mannaa, Thierry Coquand
A constructive version of Newton-Puiseux theorem for computing the Puiseux expansions of algebraic curves is presented. The proof is based on a classical proof by Abhyankar. Algebr…