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

A
Abelt, Lukas	LayeredTypes - Combining dependent and independent type systems
Accattoli, Beniamino	Normal Form Bisimulations by Value
Adjedj, Arthur	Engineering logical relations for MLTT in Coq
Ahrens, Benedikt	Formalized non-wellfounded syntax through monoidal categories
Alhabardi, Fahad	A simple model of smart contracts in Agda
Altenkirch, Thorsten	Towards dependent combinator calculus Revisiting Containers in Cubical Agda
Altenmüller, Malin	Read the mode and stay positive
B
Bach Poulsen, Casper	Types and Semantics of Extensible Data Types
Bahr, Patrick	Modal Types for Asynchronous FRP
Barras, Bruno	A graphical interface for diagrammatic proofs in proof assistants
Blot, Valentin	Diller-Nahm Bar Recursion
Borthelle, Peio	Games and Strategies using Coinductive Types
Botta, Nicola	Extensional Equality Preservation in Intensional MLTT
Bradley, Felix	On the Metatheory of Subtype Universes
Brede, Nuria	Extensional Equality Preservation in Intensional MLTT
Buchholtz, Ulrik	On epimorphisms and acyclic types in univalent type theory
C
Cagne, Pierre	Partiality Wrecks GADTs' Functoriality
Ceulemans, Joris	Read the mode and stay positive
Chabassier, Luc	A graphical interface for diagrammatic proofs in proof assistants
Chapman, James	Program logics for ledgers
Chen, Joshua	Categories as Semicategories with Identities
Cockx, Jesper	Building an elaborator using extensible constraints Operations On Syntax Should Not Inspect The Scope
Cohen, Liron	Monadic Realizability for Intuitionistic Higher-Order Logic
Coraglia, Greta	Categorical models of subtyping
Cruz-Filipe, Luís	Choreographic Programming in Coq
D
da Rocha Paiva, Bruno	Markov’s Principles in Constructive Type Theory
Damato, Stefania	Revisiting Containers in Cubical Agda
de Jong, Tom	Categories as Semicategories with Identities On epimorphisms and acyclic types in univalent type theory The ordinals in set theory and type theory are the same
Dudenhefner, Andrej	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
E
Eberl, Matthias	Dynamic Type Theory
Emmenegger, Jacopo	Categorical models of subtyping
Escot, Lucas	Read the mode and stay positive
Espírito Santo, José	Terms as Types: Calculations in the lambda-Calculus Consequences of the modal unification of the functional calling paradigms
F
Faggian, Claudia	Normal Form Bisimulations by Value
Felicissimo, Thiago	A Logical Framework for Computational Type Theories
Fonseca, Alcides	LayeredTypes - Combining dependent and independent type systems
Forster, Yannick	Markov’s Principles in Constructive Type Theory
G
Gabbay, Murdoch J.	Nominal techniques as an Agda library
Gavazzo, Francesco	Monadic Intersection Types
Gazzari, René	Terms as Types: Calculations in the lambda-Calculus
Geuvers, Herman	Self-contained rules for classical and intuitionistic quantifiers
Gilbert, Gaëtan	From Lost to the River: Embracing Sort Proliferation The Rewster: The Coq Proof Assistant with Rewrite Rules
Greenberg, Michael	Towards a Translation from Liquid Haskell to Coq
Grunfeld, Ariel	Monadic Realizability for Intuitionistic Higher-Order Logic
H
Herbelin, Hugo	New Observations on the Constructive Content of First-Order Completeness Theorems Higher coherence equations of semi-simplicial types as n-cubes of proofs
Hirschowitz, Tom	Games and Strategies using Coinductive Types
Hurkens, Tonny	Self-contained rules for classical and intuitionistic quantifiers
J
Jaber, Guilhem	Games and Strategies using Coinductive Types
Jansson, Patrik	Extensional Equality Preservation in Intensional MLTT
Johann, Patricia	Partiality Wrecks GADTs' Functoriality
Jubert, Moana	Higher coherence equations of semi-simplicial types as n-cubes of proofs
K
Kaposi, Ambrus	Towards dependent combinator calculus Towards quotient inductive-inductive-recursive types
Karkour, Ammar	A Formalization of Python's Execution Machinery
Kirst, Dominik	New Observations on the Constructive Content of First-Order Completeness Theorems Markov’s Principles in Constructive Type Theory
Konecny, Michal	Extending cAERN to spaces of subsets
Kovács, András	Efficient Evaluation for Cubical Type Theories
Kraus, Nicolai	Categories as Semicategories with Identities The ordinals in set theory and type theory are the same
Krishnaswami, Neel	Decidable Type-Checking for Bidirectional Martin-Löf Type Theory
L
Laarmann, Felix	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
Lancelot, Adrienne	Normal Form Bisimulations by Value
Lennon-Bertrand, Meven	Decidable Type-Checking for Bidirectional Martin-Löf Type Theory Engineering logical relations for MLTT in Coq
Leray, Yann	The Rewster: The Coq Proof Assistant with Rewrite Rules
Liesnikov, Bohdan	Building an elaborator using extensible constraints
Lugović, Lovro	Choreographic Programming in Coq
Luo, Zhaohui	On the Metatheory of Subtype Universes
M
Mahboubi, Assia	Manifest Termination
Maillard, Kenji	Engineering logical relations for MLTT in Coq
Manea, Cosmin	Classification of Covering Spaces and Canonical Change of Basepoint
Mastorou, Lykourgos	Towards a Translation from Liquid Haskell to Coq
Matthes, Ralph	Formalized non-wellfounded syntax through monoidal categories
McDermott, Dylan	Consequences of the modal unification of the functional calling paradigms
Melkonian, Orestis	Nominal techniques as an Agda library Program logics for ledgers
Melliès, Paul-André	Profinite lambda-terms and parametricity.
Melquiond, Guillaume	Manifest Termination
Montesi, Fabrizio	Choreographic Programming in Coq
Moreau, Vincent	Profinite lambda-terms and parametricity.
Møgelberg, Rasmus Ejlers	Modal Types for Asynchronous FRP
N
Neumann, Jacob	Categorical Logic in Lean
Nordvall Forsberg, Fredrik	The ordinals in set theory and type theory are the same
North, Paige	Coinductive control of inductive data types
Nuyts, Andreas	Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory Read the mode and stay positive A Lock Calculus for Multimode Type Theory
O
Otten, Daniël	Conservativity of Type Theory over Higher-order Arithmetic
P
Park, Sewon	Extending cAERN to spaces of subsets
Peressotti, Marco	Choreographic Programming in Coq
Pinto, Luís	Terms as Types: Calculations in the lambda-Calculus Consequences of the modal unification of the functional calling paradigms
Poiret, Josselin	Read the mode and stay positive
Portegies, Jim	Classification of Covering Spaces and Canonical Change of Basepoint
Pradal, Stiephen	Categories as Semicategories with Identities
Pujet, Loic	Engineering logical relations for MLTT in Coq
Pédrot, Pierre-Marie	From Lost to the River: Embracing Sort Proliferation
Péroux, Maximilien	Coinductive control of inductive data types
R
Rahli, Vincent	Markov’s Principles in Constructive Type Theory
Rasmussen, Robert R.	Choreographic Programming in Coq
Rehof, Jakob	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
Reis, Giselle	Formalization of Blockchain Oracles in Coq A Formalization of Python's Execution Machinery
Richter, Tim	Extensional Equality Preservation in Intensional MLTT
Rijke, Egbert	On epimorphisms and acyclic types in univalent type theory
S
Sakaguchi, Kazuhiko	A record expansion translation for Coq
Scholz, Sven-Bodo	Rank-polymorphic arrays within dependently-typed langauges
Setzer, Anton	A simple model of smart contracts in Agda
Shaheer, Mohammad	Formalization of Blockchain Oracles in Coq
Sinkarovs, Artjoms	Towards dependent combinator calculus Rank-polymorphic arrays within dependently-typed langauges
Slagel, J. Tanner	Embedding Differential Temporal Dynamic Logic in PVS
Sozeau, Matthieu	From Lost to the River: Embracing Sort Proliferation
Stahl, Christoph	Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
Swierstra, Wouter	Program logics for ledgers
T
Tabareau, Nicolas	From Lost to the River: Embracing Sort Proliferation The Rewster: The Coq Proof Assistant with Rewrite Rules
Takahashi, Yuta	Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
Tate, Ross	Monadic Realizability for Intuitionistic Higher-Order Logic
Thies, Holger	Extending cAERN to spaces of subsets
Titolo, Laura	Embedding Differential Temporal Dynamic Logic in PVS
Treglia, Riccardo	Monadic Intersection Types
U
Uustalu, Tarmo	Consequences of the modal unification of the functional calling paradigms
V
van den Berg, Benno	Conservativity of Type Theory over Higher-order Arithmetic
van der Rest, Cas	Types and Semantics of Extensible Data Types
van der Weide, Niels	Enriched Categories in Univalent Foundations Rezk Completion of Structured Categories
van Gool, Sam	Profinite lambda-terms and parametricity.
Vanoni, Gabriele	Monadic Intersection Types
Vazou, Niki	Towards a Translation from Liquid Haskell to Coq
Végh, Tamás	Towards dependent combinator calculus
W
Wemmenhove, Jelle	Classification of Covering Spaces and Canonical Change of Basepoint
White, Lauren	Embedding Differential Temporal Dynamic Logic in PVS
Winterhalter, Théo	The Rewster: The Coq Proof Assistant with Rewrite Rules Composable partial functions in Coq, totally for free
Woltzenlogel Paleo, Bruno	Formalization of Blockchain Oracles in Coq
Wullaert, Kobe	Formalized non-wellfounded syntax through monoidal categories Rezk Completion of Structured Categories
X
Xu, Chuangjie	The ordinals in set theory and type theory are the same
Z
Zakowski, Yannick	Games and Strategies using Coinductive Types

Disclaimer | Powered by EasyChair Smart Program