5 papers
Non-Derivability Results in Polymorphic Dependent Type Theory
Herman Geuvers
In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data typ…
Initial Algebras of Domains via Quotient Inductive-Inductive Types
Simcha van Collem, Niels van der Weide, Herman Geuvers
Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language c…
Cellular Automaton Reducibility as a Measure of Complexity for Infinite Words
Markel Zubia, Herman Geuvers
Infinite words, also known as streams, hold significant interest in computer science and mathematics, raising the natural question of how their complexity should be measured. We in…
Positive Hennessy-Milner Logic for Branching Bisimulation
Herman Geuvers, Komi Golov
Labelled transitions systems can be studied in terms of modal logic and in terms of bisimulation. These two notions are connected by Hennessy-Milner theorems, that show that two st…
Master Thesis Impredicative Encodings of Inductive and Coinductive Types
Steven Bronsveld, Herman Geuvers, Niels van der Weide
In the impredicative type theory of System F (λ2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data…