Internal effectful forcing in system T
From MaRDI portal
Cites work
- A coalgebraic view of bar recursion and bar induction
- A computational interpretation of forcing in type theory
- A Gentzen-style monadic translation of Gödel's system T
- A note on forcing and type theory
- An effectful way to eliminate addiction to dependence
- Constructivism in mathematics. An introduction. Volume I
- Continuity of Gödel's system T definable functionals via effectful forcing
- Continuous functions on final coalgebras
- Continuous functions on final coalgebras
- Gardening with the pythia a model of continuity in a dependent setting
- Higher order functions and Brouwer's thesis
- scientific article; zbMATH DE number 3573834 (Why is no real title available?)
- scientific article; zbMATH DE number 1215497 (Why is no real title available?)
- scientific article; zbMATH DE number 1478228 (Why is no real title available?)
- Inductive continuity via Brouwer trees
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On weak completeness of intuitionistic predicate logic
- Representations of stream processors using nested fixed points
- Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- When is a functional program not a functional program?
This page was built for publication: Internal effectful forcing in system T
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7296814)
