11 citations · 35 across the 11 of their papers we have counts for
12 papers
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…
Inferring Region Types via an Abstract Notion of Environment Transformation
Ulrich Schöpp, Chuangjie Xu
Region-based type systems are a powerful tool for various kinds of program analysis. We introduce a new inference algorithm for region types based on an abstract notion of environm…
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…
Autofocusing Self-Imaging: The Symmetric Pearcey Talbot-like Effect
Jiajia Zhao, You Wu, Zejia Lin +7
The Talbot like effect of symmetric Pearcey beams (SPBs) is presented numerically and experimentally in the free space. Owing to the Talbot like effect, the SPBs have the property…
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…
Circular symmetric Airy beam with the inverse propagation of the abruptly autofocusing Airy beam
Chuangjie Xu
In this letter, we introduce a new class of light beam, the circular symmetric Airy beam (CSAB), which arises from the extensions of the one dimensional (1D) spectrum of Airy beam…
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…
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani
We present three ordinal notation systems representing ordinals below in type theory, using recent type-theoretical innovations such as mutual inductive-inductive d…
A syntactic approach to continuity of T-definable functionals
Chuangjie Xu
We give a new proof of the well-known fact that all functions which are definable in Gödel's System T are continuous via a syntactic ap…