2 citations · 3 across the 2 of their papers we have counts for
5 papers
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…
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…