scientific article; zbMATH DE number 7269245
From MaRDI portal
Publication:5129941
Recommendations
- A type-theoretic foundation of delimited continuations
- scientific article; zbMATH DE number 1759490
- A type system for continuation calculus
- Univalent semantics of constructive type theories
- scientific article; zbMATH DE number 1302061
- A unified approach to type theory through a refined -calculus
- An intuitionistic theory of types with assumptions of high-arity variables
- (In)consistency of Extensions of Higher Order Logic and Type Theory
- A type-theoretic foundation of continuations and prompts
- Extensional constructs in intensional type theory
Cites work
- A computational interpretation of forcing in type theory
- A direct proof of Schwichtenberg's bar recursion closure theorem
- A functional interpretation with state
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Automated higher-order complexity analysis
- Continuous semantics for strong normalisation
- Denotational cost semantics for functional languages with inductive types
- Ein starker Normalisationssatz für die bar-rekursiven Funktionale
- scientific article; zbMATH DE number 3163761 (Why is no real title available?)
- scientific article; zbMATH DE number 956475 (Why is no real title available?)
- scientific article; zbMATH DE number 3664931 (Why is no real title available?)
- scientific article; zbMATH DE number 3216998 (Why is no real title available?)
- scientific article; zbMATH DE number 3231083 (Why is no real title available?)
- scientific article; zbMATH DE number 3259893 (Why is no real title available?)
- scientific article; zbMATH DE number 3335898 (Why is no real title available?)
- LCF considered as a programming language
- Logical Approaches to Computational Barriers
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Notions of computation and monads
- On bar recursion of types 0 and 1
- On Spector's bar recursion
- On the computational content of the axiom of choice
- Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions
- Strong normalisation for applied lambda calculi
- Strong normalization of barrecursive terms without using infinite terms
- Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
- Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation in the proof-system \texttt{MinLog}
- System T and the product of selection functions
- Validating Brouwer's continuity principle for numbers using named exceptions
Cited in
(3)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5129941)
