constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Synthetic Tait computability is an approach to constructing logical relations (also known as Tait’s method of computability) using the internal language of toposes constructed using Artin gluing.
Note that despite the name, synthetic Tait computability is not a subfield of synthetic computability theory, but rather a synthetic approach to Tait's method of computability. This suggests that synthetic Tait computability is one technique in a larger field of synthetic mathematics internal to a glued topos.
Jonathan Sterling, First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory, (PhD thesis)
Jonathan Sterling, Naïve logical relations in synthetic Tait computability, (pdf)
Further references are documented on Jon Sterling’s personal website.
Last revised on June 26, 2024 at 22:38:00. See the history of this page for a list of all contributions to it.