TYPES 2024: TYPES 2024

This page contains an index consisting of author-provided keywords.

A
abstraction theorem	Internal relational parametricity, without an interval
Agda	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness Mechanizing BFT consensus protocols in Agda Limited Principles of Omniscience in Constructive Type Theory
Algebraic topology	A Constructive Cellular Approximation Theorem in HoTT
almost full relations	Quasi Morphisms for Almost Full Relations
alpha-normalisation	Strict syntax of type theory via alpha-normalisation
Apartness	Harmony in Duality
As-patterns	How much do System T recursors lift to dependent types?
axiomatic type theory	Semantics of Axiomatic Type Theory
B
B-system	Type theory in type theory using single substitutions
BFT	Mechanizing BFT consensus protocols in Agda
blockchain	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness Mechanizing BFT consensus protocols in Agda
C
C-system	Type theory in type theory using single substitutions
canonical form	A Canonical Form for Universe Levels in Impredicative Type Theory
Case trees	A generic translation from case trees to eliminators
categorical semantics	The Internal Language of Univalent Categories
categories with families	Coherent Categories with Families
category theory	A directed homotopy type theory for 1-categories Updates on Paranatural Category Theory The Univalence Maxim and Univalent Double Categories
category with families	Strict syntax of type theory via alpha-normalisation Type theory in type theory using single substitutions
Church Thesis	“Proofs are programs” in MLTT
Classical Predicate Logic	Normalization of Natural Deduction for Classical Predicate Logic
Cocon	Cocon: A Type-Theoretic Framework for Meta-Programming
coherence	Coherent Categories with Families
Cohomology Operations	Revisiting the Steenrod Squares in HoTT
coinduction	Type-Based Termination Checking in Agda
coinductive proof search	Faithful interpretations of LJT and LJQ into polarized logic
Comodules	Comodule Representations of Second-Order Functionals
completions	Identity types in predicate logic
comprehension categories	The Internal Language of Univalent Categories
comprehension category	Semantics of Axiomatic Type Theory
Computability theory	Post’s Problem and the Priority Method in CIC Oracle modalities
consensus	Mechanizing BFT consensus protocols in Agda
Constructive Mathematics	Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues A Constructive Cellular Approximation Theorem in HoTT Limited Principles of Omniscience in Constructive Type Theory Revisiting the Steenrod Squares in HoTT Constructive Ordinal Exponentiation in Homotopy Type Theory A zoo of continuity properties in constructive type theory
constructive reverse mathematics	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem A zoo of continuity properties in constructive type theory
Constructive type theory	Post’s Problem and the Priority Method in CIC Limited Principles of Omniscience in Constructive Type Theory
constructive well quasi ordering	Quasi Morphisms for Almost Full Relations
Constructivity questions	Recent progress in the theory of effective Kan fibrations in simplicial sets
Containers	Comodule Representations of Second-Order Functionals
continuity	A zoo of continuity properties in constructive type theory
Coq	A formal security analysis of Blockchain voting Yet another formal theory of probabilities (with an application to random sampling) “Proofs are programs” in MLTT Post’s Problem and the Priority Method in CIC The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem A zoo of continuity properties in constructive type theory Quasi Morphisms for Almost Full Relations
Cubical Agda	Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues
cubical sets	Oracle modalities
Cubical Type Theory	Universes in simplicial type theory Poset Type Theory
D
dependent choice	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem
Dependent type theory	Towards Quantitative Inductive Families A modal deconstruction of Loeb induction Harmony in Duality Extensional Finite Sets and Multisets in Type Theory
Dependent types	Towards a logical framework modulo rewriting and equational theories A generic translation from case trees to eliminators Splitting Booleans with Normalization-by-Evaluation Type-Based Termination Checking in Agda
directed homotopy type theory	A directed homotopy type theory for 1-categories
directed type theory	Universes in simplicial type theory
directed univalence	Universes in simplicial type theory
Discrete probability theory
display map	Semantics of Axiomatic Type Theory
doctrines	Identity types in predicate logic
double categories	The Univalence Maxim and Univalent Double Categories
drinker paradox	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem
E
eBPF	Proof and Consequences: Separating Construction and Checking of eBPF Loops
Effects	Limited Principles of Omniscience in Constructive Type Theory
Effectus theory
Elaboration	A generic translation from case trees to eliminators
Elimination	A generic translation from case trees to eliminators
Equality	Harmony in Duality
Equational theory	Towards a logical framework modulo rewriting and equational theories
equivalence	Semantics of Axiomatic Type Theory
Ethereum	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Explicit Mathmematics	Predicativity of the Mahlo Universe in Type Theory
exponentiation	Constructive Ordinal Exponentiation in Homotopy Type Theory
extended-predicative	Predicativity of the Mahlo Universe in Type Theory
Extensionality	Splitting Booleans with Normalization-by-Evaluation
extrinsic syntax	Strict syntax of type theory via alpha-normalisation
F
fibration	Semantics of Axiomatic Type Theory
fibrations	Universes in simplicial type theory
focusing	Faithful interpretations of LJT and LJQ into polarized logic
Formalisation of mathematics	Concrete Univalent Mathematics
formalization	Yet another formal theory of probabilities (with an application to random sampling)
formalization of mathematics	The Univalence Maxim and Univalent Double Categories
Free algebraic structures	Extensional Finite Sets and Multisets in Type Theory
functional programming	Updates on Paranatural Category Theory
G
Groupoids	Partial Combinatory Algebras for Intensional Type Theory
Guard condition	Size-preserving dependent elimination
Guarded recursion	A modal deconstruction of Loeb induction
H
Hacspec	A formal security analysis of Blockchain voting
higher topos theory	Synthetic Stone duality
Hoare logic	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
homotopy	Semantics of Axiomatic Type Theory
Homotopy theory	A Constructive Cellular Approximation Theorem in HoTT
homotopy type theory	Coherent Categories with Families Univalent Material Set Theory: Hierarchies of n-types Comparing Quotient- and Symmetric Containers Oracle modalities A modal deconstruction of Loeb induction Revisiting the Steenrod Squares in HoTT Synthetic Stone duality Constructive Ordinal Exponentiation in Homotopy Type Theory Concrete Univalent Mathematics
HoTT	A Constructive Cellular Approximation Theorem in HoTT
I
identity types	Identity types in predicate logic
imax algebra	A Canonical Form for Universe Levels in Impredicative Type Theory
Implementation of Type Theory	Poset Type Theory
impredicativity	A Canonical Form for Universe Levels in Impredicative Type Theory
Inductive data types	Extensional Finite Sets and Multisets in Type Theory
Inductive families	Towards Quantitative Inductive Families
Inductive-coinductive types	Harmony in Duality
Inductive-recursive definitions	Predicativity of the Mahlo Universe in Type Theory
inhabitation	Faithful interpretations of LJT and LJQ into polarized logic
Intensional type theory	Partial Combinatory Algebras for Intensional Type Theory
internal parametricity	Internal relational parametricity, without an interval
intersection types	Useful Evaluation, Quantitatively
intrinsic syntax	Strict syntax of type theory via alpha-normalisation
Inverse computing	Looking Back: A Probabilistic Inverse Perspective on Test Generation
invited talk	Cocon: A Type-Theoretic Framework for Meta-Programming Bridging Neural and Symbolic Proof Automation
L
lambda calculus	Useful Evaluation, Quantitatively
Limited Principle of Omniscience	Limited Principles of Omniscience in Constructive Type Theory
Logic	Representing Temporal Operators with Dependent Event Types Logic in Dependent Type Theory
Logical Foundations	Limited Principles of Omniscience in Constructive Type Theory
Logical framework	Towards a logical framework modulo rewriting and equational theories
logical relation	“Proofs are programs” in MLTT
Löwenheim-Skolem theorem	The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem
M
Mahlo cardinal	Predicativity of the Mahlo Universe in Type Theory
Mahlo Universe	Predicativity of the Mahlo Universe in Type Theory
Mahlo universes	Large Universe Construction by Indexed Induction-Recursion in Agda
Martin-Löf type theory	Predicativity of the Mahlo Universe in Type Theory Large Universe Construction by Indexed Induction-Recursion in Agda Strict syntax of type theory via alpha-normalisation Type theory in type theory using single substitutions Internal relational parametricity, without an interval
material set theory	Univalent Material Set Theory: Hierarchies of n-types
Mathematical Components	Yet another formal theory of probabilities (with an application to random sampling)
meaning explanations	Predicativity of the Mahlo Universe in Type Theory
mechanization	Mechanizing BFT consensus protocols in Agda Quasi Morphisms for Almost Full Relations
Meta programming	Cocon: A Type-Theoretic Framework for Meta-Programming
MLTT	“Proofs are programs” in MLTT
Modal type theory	A directed homotopy type theory for 1-categories A modal deconstruction of Loeb induction
Modalities	A modal deconstruction of Loeb induction
model	Semantics of Axiomatic Type Theory
monad transformers	Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time
Monads	Comodule Representations of Second-Order Functionals
morphisms	Quasi Morphisms for Almost Full Relations
multimodal type theory	Universes in simplicial type theory
N
Natural Deduction	Normalization of Natural Deduction for Classical Predicate Logic
natural language	Representing Temporal Operators with Dependent Event Types
Normalisation by Evaluation	Implementing Observational Equality with Normalisation by Evaluation Splitting Booleans with Normalization-by-Evaluation
Normalization	Normalization of Natural Deduction for Classical Predicate Logic
O
objective type theory	Semantics of Axiomatic Type Theory
Observational Equality	Implementing Observational Equality with Normalisation by Evaluation
Observational type theory	Harmony in Duality
Open Vote Network	A formal security analysis of Blockchain voting
ordinals	Constructive Ordinal Exponentiation in Homotopy Type Theory
P
parametric polymorphism	Updates on Paranatural Category Theory
Partial combinatory algebras	Partial Combinatory Algebras for Intensional Type Theory
partial equivalence relations	Identity types in predicate logic
path category	Semantics of Axiomatic Type Theory
Pattern-matching	How much do System T recursors lift to dependent types? A generic translation from case trees to eliminators
Peter Aczel	On Relating Type Theories and Set Theories Logic in Dependent Type Theory Special Session in Memory of Peter Aczel
polarization	Faithful interpretations of LJT and LJQ into polarized logic
polymorphism	Type-Based Termination Checking in Agda
Postcondition	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Precondition	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
predicativity	Predicativity of the Mahlo Universe in Type Theory
Probabilistic computing	Looking Back: A Probabilistic Inverse Perspective on Test Generation
Probabilistic logic
probability theory	Yet another formal theory of probabilities (with an application to random sampling)
Proof as terms	Normalization of Natural Deduction for Classical Predicate Logic
Proof assistant	OnlineProver: A proof assistant for online teaching of formal logic and semantics
proof automation	Bridging Neural and Symbolic Proof Automation
Proof-irrelevant propositional equality	Size-preserving dependent elimination
Propositional extensionality	Size-preserving dependent elimination
propositional type theory	Semantics of Axiomatic Type Theory
Prototype implementation	Implementing Observational Equality with Normalisation by Evaluation
Provable correctness	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Q
quantitative models	Useful Evaluation, Quantitatively
Quantitative type theory	Towards Quantitative Inductive Families
quote	“Proofs are programs” in MLTT
quotient containers	Comparing Quotient- and Symmetric Containers
R
realizability	Partial Combinatory Algebras for Intensional Type Theory Oracle modalities
Recursion	How much do System T recursors lift to dependent types?
relational parametricity	Internal relational parametricity, without an interval
Representations	Comodule Representations of Second-Order Functionals
Rewriting	Towards a logical framework modulo rewriting and equational theories
Rezk completions	A formal study of the Rezk completion
Rezk types	Universes in simplicial type theory
S
Schemes	Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues
Second-Order Functionals	Comodule Representations of Second-Order Functionals
Security	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Segal types	Universes in simplicial type theory
Semantics of type theory	Recent progress in the theory of effective Kan fibrations in simplicial sets
sequent calculus	Faithful interpretations of LJT and LJQ into polarized logic
Set Theory	On Relating Type Theories and Set Theories
sheaf models	Synthetic Stone duality
Simplicial sets	Recent progress in the theory of effective Kan fibrations in simplicial sets
simplicial type theory	Universes in simplicial type theory
single substitution	Type theory in type theory using single substitutions
sized types	Type-Based Termination Checking in Agda
Small inversion	Size-preserving dependent elimination
Smart Contract	A formal security analysis of Blockchain voting
Smart contracts	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
special session	Special Session in Memory of Peter Aczel
staged compilation	Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time
Static analysis	Proof and Consequences: Separating Construction and Checking of eBPF Loops
Steenrod Algebras	Revisiting the Steenrod Squares in HoTT
stream fusion	Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time
Sub-formula property	Normalization of Natural Deduction for Classical Predicate Logic
symmetric containers	Comparing Quotient- and Symmetric Containers
Synethetic Homotopy Theory	Revisiting the Steenrod Squares in HoTT
synthetic algebraic geometry	Synthetic Stone duality
Synthetic computability	Post’s Problem and the Priority Method in CIC
synthetic infinity-categories	Universes in simplicial type theory
synthetic quasicoherence	Universes in simplicial type theory
System F	Updates on Paranatural Category Theory
System T	How much do System T recursors lift to dependent types?
T
TBA	Bridging Neural and Symbolic Proof Automation Special Session in Memory of Peter Aczel
Teaching theoretical CS	OnlineProver: A proof assistant for online teaching of formal logic and semantics
temporal logic	Representing Temporal Operators with Dependent Event Types
Test Generation	Looking Back: A Probabilistic Inverse Perspective on Test Generation
Theorem prover	OnlineProver: A proof assistant for online teaching of formal logic and semantics
tripos-to-topos construction	Identity types in predicate logic
Type system	Proof and Consequences: Separating Construction and Checking of eBPF Loops
Type Theory	A Constructive Cellular Approximation Theorem in HoTT Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time Representing Temporal Operators with Dependent Event Types Poset Type Theory A zoo of continuity properties in constructive type theory On Relating Type Theories and Set Theories Logic in Dependent Type Theory
type-based termination	Type-Based Termination Checking in Agda
Typed Assembly Language	Proof and Consequences: Separating Construction and Checking of eBPF Loops
U
Univalence	A modal deconstruction of Loeb induction Synthetic Stone duality Concrete Univalent Mathematics
Univalent (2-)category theory	A formal study of the Rezk completion
univalent categories	The Internal Language of Univalent Categories
univalent foundations	The Internal Language of Univalent Categories A formal study of the Rezk completion Univalent Material Set Theory: Hierarchies of n-types The Univalence Maxim and Univalent Double Categories
universe levels	A Canonical Form for Universe Levels in Impredicative Type Theory
universe operators	Large Universe Construction by Indexed Induction-Recursion in Agda
universe types	Large Universe Construction by Indexed Induction-Recursion in Agda Universes in simplicial type theory
useful evaluation	Useful Evaluation, Quantitatively
V
Verification	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
W
weak type theory	Semantics of Axiomatic Type Theory
Weakest precondition	Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
Well-founded fixpoints	Size-preserving dependent elimination
Y
Yoneda Lemma	Updates on Paranatural Category Theory

Disclaimer | Powered by EasyChair Smart Program