11 citations · 35 across the 11 of their papers we have counts for
7 papers · 1 filter
The Gentzen-style monadic translation of Gödel's System T revisited
Chuangjie Xu
We revisit the Gentzen-style monadic translation of Gödel's System T. The translation is parametrized by a nucleus, a monad-like structure that need not satisfy the monad laws. A f…
Set-Theoretic and Type-Theoretic Ordinals Coincide
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary…
Type-Theoretic Approaches to Ordinals
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate li…
Type-based Enforcement of Infinitary Trace Properties for Java
Serdar Erbatur, Ulrich Schöpp, Chuangjie Xu
A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for F…
Connecting Constructive Notions of Ordinals in Homotopy Type Theory
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and…
On the Herbrand Functional Interpretation
Paulo Oliva, Chuangjie Xu
We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication…
A Gentzen-style monadic translation of Gödel's System T
Chuangjie Xu
We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translati…