TYPES 2023: 29TH INTERNATIONAL CONFERENCE ON TYPES FOR PROOFS AND PROGRAMS

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

A
acyclic space	On epimorphisms and acyclic types in univalent type theory
AERN	Extending cAERN to spaces of subsets
Agda	A simple model of smart contracts in Agda Nominal techniques as an Agda library Markov’s Principles in Constructive Type Theory Read the mode and stay positive
Algebra	Coinductive control of inductive data types
algebraic effects	Monadic Intersection Types
arrays	Rank-polymorphic arrays within dependently-typed langauges
B
Bar recursion	Diller-Nahm Bar Recursion
bicategories	Enriched Categories in Univalent Foundations
Bidirectional Typing	Decidable Type-Checking for Bidirectional Martin-Löf Type Theory A Logical Framework for Computational Type Theories
bisimulations	Normal Form Bisimulations by Value
blockchain	Program logics for ledgers Formalization of Blockchain Oracles in Coq
C
Calculation term	Terms as Types: Calculations in the lambda-Calculus
Calculus of Inductive Constructions	New Observations on the Constructive Content of First-Order Completeness Theorems Conservativity of Type Theory over Higher-order Arithmetic
call-by-box	Consequences of the modal unification of the functional calling paradigms
call-by-name	Consequences of the modal unification of the functional calling paradigms
call-by-push-value	Consequences of the modal unification of the functional calling paradigms
call-by-value	Consequences of the modal unification of the functional calling paradigms
categorical diagrams	A graphical interface for diagrammatic proofs in proof assistants
categorical logic	Categorical Logic in Lean Categorical models of subtyping
categories with families	Categorical models of subtyping
category theory	Rezk Completion of Structured Categories Categorical Logic in Lean Categories as Semicategories with Identities Enriched Categories in Univalent Foundations
Change of Basepoint	Classification of Covering Spaces and Canonical Change of Basepoint
choreographic programming	Choreographic Programming in Coq
Church encoding	Profinite lambda-terms and parametricity.
classical and intuitionistic logic	Self-contained rules for classical and intuitionistic quantifiers
coalgebra	Coinductive control of inductive data types
coercive subtyping	On the Metatheory of Subtype Universes
coinduction	Games and Strategies using Coinductive Types Formalized non-wellfounded syntax through monoidal categories
combinatory logic	Towards dependent combinator calculus Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
completeness theorems	New Observations on the Constructive Content of First-Order Completeness Theorems
compositionality	Composable partial functions in Coq, totally for free
Computable Analysis	Extending cAERN to spaces of subsets
concurrency	Rank-polymorphic arrays within dependently-typed langauges
concurrent systems	Choreographic Programming in Coq
Conservativity	Conservativity of Type Theory over Higher-order Arithmetic
constructive mathematics	Monadic Realizability for Intuitionistic Higher-Order Logic
constructive reverse mathematics	New Observations on the Constructive Content of First-Order Completeness Theorems
constructive set theory	Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe The ordinals in set theory and type theory are the same
constructive type theory	Markov’s Principles in Constructive Type Theory
constructivism	Monadic Realizability for Intuitionistic Higher-Order Logic
containers	Revisiting Containers in Cubical Agda
Coq	A record expansion translation for Coq Extending cAERN to spaces of subsets Rezk Completion of Structured Categories Markov’s Principles in Constructive Type Theory The Rewster: The Coq Proof Assistant with Rewrite Rules Composable partial functions in Coq, totally for free Enriched Categories in Univalent Foundations Formalized non-wellfounded syntax through monoidal categories
Covering Spaces	Classification of Covering Spaces and Canonical Change of Basepoint
cubical agda	Revisiting Containers in Cubical Agda
cubical type theory	Efficient Evaluation for Cubical Type Theories
cumulative hierarchy	The ordinals in set theory and type theory are the same
Curry-Howard correspondence	Terms as Types: Calculations in the lambda-Calculus
D
degrees of relatedness	Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory
dependent record	A record expansion translation for Coq
dependent type theory	A record expansion translation for Coq Read the mode and stay positive Categorical models of subtyping
dependent types	Towards dependent combinator calculus Rank-polymorphic arrays within dependently-typed langauges On the Metatheory of Subtype Universes Building an elaborator using extensible constraints Decidable Type-Checking for Bidirectional Martin-Löf Type Theory
Dependently typed programming	Operations On Syntax Should Not Inspect The Scope
Dialectica	Diller-Nahm Bar Recursion
Differential Dynamic Logic	Embedding Differential Temporal Dynamic Logic in PVS
Diller-Nahm	Diller-Nahm Bar Recursion
distributed ledgers	Program logics for ledgers
dynamic	Dynamic Type Theory
E
effects	Monadic Realizability for Intuitionistic Higher-Order Logic Markov’s Principles in Constructive Type Theory
elaboration	Building an elaborator using extensible constraints
elaborator reflection	Nominal techniques as an Agda library
elaborators	Building an elaborator using extensible constraints
Elpi	A record expansion translation for Coq
Embedding	On the Metatheory of Subtype Universes Embedding Differential Temporal Dynamic Logic in PVS
enriched categories	Enriched Categories in Univalent Foundations
enriched category theory	Coinductive control of inductive data types
epimorphism	On epimorphisms and acyclic types in univalent type theory
Equality	Terms as Types: Calculations in the lambda-Calculus
Ethereum	A simple model of smart contracts in Agda
Ethereum Virtual Machine	A simple model of smart contracts in Agda
evaluation	Efficient Evaluation for Cubical Type Theories
Exact real computation	Extending cAERN to spaces of subsets
Execution Model	A simple model of smart contracts in Agda
extensible datatype	Building an elaborator using extensible constraints
F
fibrations	Categorical models of subtyping
finite semantics	Profinite lambda-terms and parametricity.
finitism	Dynamic Type Theory
First-order logic	Terms as Types: Calculations in the lambda-Calculus
Formal proof	Engineering logical relations for MLTT in Coq
Formal Verification	Formalization of Blockchain Oracles in Coq
formal verification	Program logics for ledgers
formalisation	Composable partial functions in Coq, totally for free Revisiting Containers in Cubical Agda
Fstar	A Formalization of Python's Execution Machinery
Function Extensionality	Extensional Equality Preservation in Intensional MLTT
Functional reactive programming	Modal Types for Asynchronous FRP
Functorial semantics	Partiality Wrecks GADTs' Functoriality
functorial strength	Formalized non-wellfounded syntax through monoidal categories
G
GADTs	Partiality Wrecks GADTs' Functoriality
general recursion	Composable partial functions in Coq, totally for free
graphical interface	A graphical interface for diagrammatic proofs in proof assistants
Guarded recursion	Modal Types for Asynchronous FRP
H
Heyting Arithmetic	Conservativity of Type Theory over Higher-order Arithmetic
higher coherence equations	Higher coherence equations of semi-simplicial types as n-cubes of proofs
higher-order automata	Profinite lambda-terms and parametricity.
higher-order logic	Monadic Realizability for Intuitionistic Higher-Order Logic Conservativity of Type Theory over Higher-order Arithmetic
Hoare logic	Program logics for ledgers
homotopy type theory	Rezk Completion of Structured Categories Higher coherence equations of semi-simplicial types as n-cubes of proofs Classification of Covering Spaces and Canonical Change of Basepoint Categories as Semicategories with Identities Enriched Categories in Univalent Foundations The ordinals in set theory and type theory are the same On epimorphisms and acyclic types in univalent type theory
I
idempotent equivalence	Categories as Semicategories with Identities
identities	Categories as Semicategories with Identities
implementation	Efficient Evaluation for Cubical Type Theories
indefinitely large finite	Dynamic Type Theory
independence	Markov’s Principles in Constructive Type Theory
induction-recursion	Towards quotient inductive-inductive-recursive types
inductive types	Towards quotient inductive-inductive-recursive types Read the mode and stay positive Revisiting Containers in Cubical Agda
inhabitation problem	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
Intensional Type Theory	Extensional Equality Preservation in Intensional MLTT
interactive theorem proving	Categorical Logic in Lean
internal language	Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory
Interpreters	A Formalization of Python's Execution Machinery
intersection types	Monadic Intersection Types Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
intuitionistic logic	Monadic Realizability for Intuitionistic Higher-Order Logic
K
Kripke semantics	Self-contained rules for classical and intuitionistic quantifiers
L
labelled transition system	Games and Strategies using Coinductive Types
lambda-calculus	Normal Form Bisimulations by Value
language design	Types and Semantics of Extensible Data Types
Lean proof assistant	Categorical Logic in Lean
Lindenbaum-Tarski algebras	Categorical Logic in Lean
Linear Temporal Logic	Embedding Differential Temporal Dynamic Logic in PVS
linear type theory	A Lock Calculus for Multimode Type Theory
Liquid Haskell	Towards a Translation from Liquid Haskell to Coq
Liquid Types	LayeredTypes - Combining dependent and independent type systems
Logic and verification	A Formalization of Python's Execution Machinery
Logical Frameworks	A Logical Framework for Computational Type Theories
M
Mahlo universes	Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
Markov's principle	Markov’s Principles in Constructive Type Theory
Martin-Lof type theory	Conservativity of Type Theory over Higher-order Arithmetic
Martin-Löf type theory	Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
mathematical structures	A record expansion translation for Coq
metacoq	The Rewster: The Coq Proof Assistant with Rewrite Rules
modal embedding	Consequences of the modal unification of the functional calling paradigms
modal logic S4	Consequences of the modal unification of the functional calling paradigms
modal type theory	Read the mode and stay positive A Lock Calculus for Multimode Type Theory
Modal types	Modal Types for Asynchronous FRP
modularity	Types and Semantics of Extensible Data Types
monads	Monadic Realizability for Intuitionistic Higher-Order Logic Monadic Intersection Types Categorical Logic in Lean
monoidal category	Formalized non-wellfounded syntax through monoidal categories
MTT	A Lock Calculus for Multimode Type Theory
Muenchhausen	Towards dependent combinator calculus
multimodal type theory	A Lock Calculus for Multimode Type Theory
multimode type theory	A Lock Calculus for Multimode Type Theory
N
n-cube	Higher coherence equations of semi-simplicial types as n-cubes of proofs
Natural calculations	Terms as Types: Calculations in the lambda-Calculus
natural deduction for predicate logic	Self-contained rules for classical and intuitionistic quantifiers
new predicate logic quantifiers	Self-contained rules for classical and intuitionistic quantifiers
nominal techniques	Nominal techniques as an Agda library
non-idempotent intersection types	Normal Form Bisimulations by Value
O
Object-oriented languages	A Formalization of Python's Execution Machinery
omega-continuous functor	Formalized non-wellfounded syntax through monoidal categories
open datatype	Building an elaborator using extensible constraints
operational game semantics	Games and Strategies using Coinductive Types
Operational semantics	A Formalization of Python's Execution Machinery
Oracle	Formalization of Blockchain Oracles in Coq
ordered type theory	A Lock Calculus for Multimode Type Theory
ordinal	The ordinals in set theory and type theory are the same
P
parallelism	Rank-polymorphic arrays within dependently-typed langauges
parametricity	Profinite lambda-terms and parametricity. Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory
partial combinatory algebras	Monadic Realizability for Intuitionistic Higher-Order Logic
partial function	Composable partial functions in Coq, totally for free
Partial functions	Partiality Wrecks GADTs' Functoriality
Partial morphisms	Partiality Wrecks GADTs' Functoriality
polarity annotations	Read the mode and stay positive
potential infinite	Dynamic Type Theory
potentialist	Dynamic Type Theory
Preservation of extensional equality	Extensional Equality Preservation in Intensional MLTT
presheaf models	Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory
profinite spaces	Profinite lambda-terms and parametricity.
program equivalence	Normal Form Bisimulations by Value
Program Extraction	Extending cAERN to spaces of subsets
program semantics	Program logics for ledgers
proof assistant	The Rewster: The Coq Proof Assistant with Rewrite Rules
Proof assistants	Engineering logical relations for MLTT in Coq A graphical interface for diagrammatic proofs in proof assistants
proof automation	Categorical Logic in Lean
proof tactics	Categorical Logic in Lean
Proof term	Terms as Types: Calculations in the lambda-Calculus
Proofs engineering	Engineering logical relations for MLTT in Coq
PVS	Embedding Differential Temporal Dynamic Logic in PVS
Python bytecode	A Formalization of Python's Execution Machinery
Q
quotient inductive types	Towards quotient inductive-inductive-recursive types
R
rank polymorphism	Rank-polymorphic arrays within dependently-typed langauges
Reader monad	Extensional Equality Preservation in Intensional MLTT
realizability	Monadic Realizability for Intuitionistic Higher-Order Logic
reduction	Manifest Termination
refinement types	Towards a Translation from Liquid Haskell to Coq
regular languages	Profinite lambda-terms and parametricity.
rewrite rules	The Rewster: The Coq Proof Assistant with Rewrite Rules
Rezk completion	Rezk Completion of Structured Categories
Run-time erasure	Operations On Syntax Should Not Inspect The Scope
S
Semantics	A Formalization of Python's Execution Machinery
Semantics and reasoning	A Formalization of Python's Execution Machinery
semi-simplicial types	Higher coherence equations of semi-simplicial types as n-cubes of proofs
semicategories	Categories as Semicategories with Identities
separation logic	Program logics for ledgers
set-theoretic types	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
simply-typed lambda-calculus	Profinite lambda-terms and parametricity.
Smart Contracts	A simple model of smart contracts in Agda
Solidity	A simple model of smart contracts in Agda
sorts	From Lost to the River: Embracing Sort Proliferation
Spaces of subsets	Extending cAERN to spaces of subsets
Static Verification	LayeredTypes - Combining dependent and independent type systems
strictification	Towards quotient inductive-inductive-recursive types
strictly positive	Revisiting Containers in Cubical Agda
subformula property	Self-contained rules for classical and intuitionistic quantifiers
subtype universes	On the Metatheory of Subtype Universes
subtyping	On the Metatheory of Subtype Universes Categorical models of subtyping
Syntax	A Formalization of Python's Execution Machinery
Synthetic Homotopy Theory	Classification of Covering Spaces and Canonical Change of Basepoint
T
termination	Manifest Termination
theorem proving	Towards a Translation from Liquid Haskell to Coq Choreographic Programming in Coq
Topological spaces	Extending cAERN to spaces of subsets
topos theory	Monadic Realizability for Intuitionistic Higher-Order Logic
Traversable functors	Extensional Equality Preservation in Intensional MLTT
triposes	Monadic Realizability for Intuitionistic Higher-Order Logic
two-level type theory	Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory
Type systems	Types and Semantics of Extensible Data Types LayeredTypes - Combining dependent and independent type systems
type theory	On the Metatheory of Subtype Universes Manifest Termination From Lost to the River: Embracing Sort Proliferation The Rewster: The Coq Proof Assistant with Rewrite Rules Engineering logical relations for MLTT in Coq Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis A Logical Framework for Computational Type Theories
type theory in type theory	Towards quotient inductive-inductive-recursive types
type-checking	Building an elaborator using extensible constraints Decidable Type-Checking for Bidirectional Martin-Löf Type Theory
U
UniMath library	Formalized non-wellfounded syntax through monoidal categories
univalent foundations	Rezk Completion of Structured Categories Enriched Categories in Univalent Foundations On epimorphisms and acyclic types in univalent type theory
universe polymorphism	From Lost to the River: Embracing Sort Proliferation
untyped λ-calculus	Nominal techniques as an Agda library
UTxO	Program logics for ledgers
V
variable binding	Nominal techniques as an Agda library
Verification	A simple model of smart contracts in Agda
Virtual machines	A Formalization of Python's Execution Machinery
W
W-types	Coinductive control of inductive data types
Weakest Precondition	A simple model of smart contracts in Agda
Well-scoped syntax	Operations On Syntax Should Not Inspect The Scope

Disclaimer | Powered by EasyChair Smart Program