20 citations · 34 across the 7 of their papers we have counts for
6 papers · 1 filter
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…
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…
Type Theory based on Dependent Inductive and Coinductive Types
Henning Basold, Herman Geuvers
We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theor…
Proceedings Fourth Workshop on Classical Logic and Computation
Herman Geuvers, Ugo de'Liguoro
CL&C'12 was the fourth of a conference series on "Classical Logic and Computation", held as satellite to ICALP'12 on Sunday July 8, 2012 in Warwick, England. CL&C intends to cover…
Degrees of Undecidability in Rewriting
Joerg Endrullis, Herman Geuvers, Hans Zantema
Undecidability of various properties of first order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. Th…