scientific article; zbMATH DE number 7199581

MaRDI QIDQ5109510

Chuangjie Xu

Publication date: 12 May 2020

Full work available at URL: https://arxiv.org/abs/1904.09794

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (3)

A universal algorithm for Krull's theorem ⋮ Unnamed Item ⋮ Higher order functions and Brouwer’s thesis

Uses Software

• Agda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Continuity of Gödel's system T definable functionals via effectful forcing
• A constructive manifestation of the Kleene-Kreisel continuous functionals
• Sheaf models for choice sequences
• Pointwise hereditary majorization and some applications
• Continuous Truth II: Reflections
• A Note on Forcing and Type Theory
• Proofs and Computations
• Logical relations and the typed λ-calculus
• On bar recursion of types 0 and 1
• A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM
• Validating Brouwer's continuity principle for numbers using named exceptions
• A Computational Interpretation of Forcing in Type Theory
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

This page was built for publication: