Thorsten Altenkirch

100 papers A* 9B 17C 2Misc 2Journal 31Unranked 32
YearRankTypeTitle / Venue / Authors
2026 J jnl
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday.
CoRR
Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani, Ugo de'Liguoro
2026 B conf
The Groupoid-Syntax of Type Theory Is a Set.
CSL
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
2025 B conf
Formalising Inductive and Coinductive Containers.
ITP
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
2025 — conf
Substitution Without Copy and Paste.
LFMTP@FSCD
Thorsten Altenkirch, Nathaniel Burke, Philip Wadler
2025 J jnl
The Groupoid-syntax of Type Theory is a Set.
CoRR
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
2024 J jnl
Formalising inductive and coinductive containers.
CoRR
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
2024 J jnl
Internal Parametricity, without an Interval.
Proc. ACM Program. Lang.
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
2024 J jnl
Preface: Advances in Homotopy Type Theory.
Math. Struct. Comput. Sci.
Thorsten Altenkirch, Benno van den Berg, Nicola Gambino, Maria Emilia Maietti
2024 — conf
Synthetic 1-Categories in Directed Type Theory.
TYPES
Jacob Neumann, Thorsten Altenkirch
2024 J jnl
Synthetic 1-Categories in Directed Type Theory.
CoRR
Thorsten Altenkirch, Jacob Neumann
2023 B conf
Combinatory Logic and Lambda Calculus Are Equal, Algebraically.
FSCD
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
2023 J jnl
Internal parametricity, without an interval.
CoRR
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
2022 — conf
The Münchhausen Method in Type Theory.
TYPES
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
2021 — ed.
26th International Conference on Types for Proofs and Programs, TYPES 2020, University of Turin, Italy, March 2-5, 2020
TYPES
Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch
2021 B conf
Constructing a universe for the setoid model.
FoSSaCS
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini
2021 J jnl
Martin Hofmann's contributions to type theory: Groupoids and univalence.
Math. Struct. Comput. Sci.
Thorsten Altenkirch
2021 J jnl
Should Type Theory replace Set Theory as the Foundation of Mathematics.
CoRR
Thorsten Altenkirch
2020 A* conf
The Integers as a Higher Inductive Type.
LICS
Thorsten Altenkirch, Luis Scoccola
2020 J jnl
The Integers as a Higher Inductive Type.
CoRR
Thorsten Altenkirch, Luis Scoccola
2019 — conf
Big Step Normalisation for Type Theory.
TYPES
Thorsten Altenkirch, Colin Geniet
2019 J jnl
Constructing quotient inductive-inductive types.
Proc. ACM Program. Lang.
Ambrus Kaposi, András Kovács, Thorsten Altenkirch
2019 J jnl
Preface.
Fundam. Informaticae
Thorsten Altenkirch, Aleksy Schubert
2019 B conf
Setoid Type Theory - A Syntactic Translation.
MPC
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
2018 A* conf
Free Higher Groups in Homotopy Type Theory.
LICS
Nicolai Kraus, Thorsten Altenkirch
2018 J jnl
Free Higher Groups in Homotopy Type Theory.
CoRR
Nicolai Kraus, Thorsten Altenkirch
2018 — conf
Pure Functional Epidemics: An Agent-Based Approach.
IFL
Jonathan Thaler, Thorsten Altenkirch, Peer-Olaf Siebers
2018 B conf
Quotient Inductive-Inductive Types.
FoSSaCS
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg
2017 J jnl
Normalisation by Evaluation for Type Theory, in Type Theory.
Log. Methods Comput. Sci.
Thorsten Altenkirch, Ambrus Kaposi
2017 J jnl
Notions of Anonymous Existence in Martin-Löf Type Theory.
Log. Methods Comput. Sci.
Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
2017 B conf
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.
FoSSaCS
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
2016 B conf
Extending Homotopy Type Theory with Strict Equality.
CSL
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
2016 J jnl
Extending Homotopy Type Theory with Strict Equality.
CoRR
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
2016 B conf
Normalisation by Evaluation for Dependent Types.
FSCD
Thorsten Altenkirch, Ambrus Kaposi
2016 J jnl
Normalisation by Evaluation for Type Theory, in Type Theory.
CoRR
Thorsten Altenkirch, Ambrus Kaposi
2016 J jnl
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.
CoRR
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
2016 J jnl
Quotient inductive-inductive types.
CoRR
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg
2016 J jnl
Selected papers from Dependently Typed Programming 2010 - Overview.
Math. Struct. Comput. Sci.
Thorsten Altenkirch, Conor McBride
2016 A* conf
Type theory in type theory using quotient inductive types.
POPL
Thorsten Altenkirch, Ambrus Kaposi
2015 — ed.
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, Warsaw, Poland, July 1-3, 2015
TLCA
Thorsten Altenkirch
2015 J jnl
Indexed containers.
J. Funct. Program.
Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, Peter Morris
2015 J jnl
Monads need not be endofunctors.
Log. Methods Comput. Sci.
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2015 — conf
Towards a Cubical Type Theory without an Interval.
TYPES
Thorsten Altenkirch, Ambrus Kaposi
2014 J jnl
Relative Monads Formalised.
J. Formaliz. Reason.
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2014 — conf
Some constructions on ω-groupoids.
LFMTP
Thorsten Altenkirch, Nuo Li, Ondrej Rypacek
2013 — conf
Generalizations of Hedberg's Theorem.
TLCA
Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch
2013 — conf
Small Induction Recursion.
TLCA
Peter G. Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch
2012 B conf
A Syntactical Approach to Weak omega-Groupoids.
CSL
Thorsten Altenkirch, Ondrej Rypacek
2011 B conf
A Categorical Semantics for Inductive-Inductive Definitions.
CALCO
Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer
2010 — conf
Hereditary Substitutions for Simple Types, Formalized.
MSFP@ICFP
Chantal Keller, Thorsten Altenkirch
2010 C conf
Higher-Order Containers.
CiE
Thorsten Altenkirch, Paul Blain Levy, Sam Staton
2010 B conf
Monads Need Not Be Endofunctors.
FoSSaCS
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2010 Misc conf
PiSigma: Dependent Types without the Sugar.
FLOPS
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury
2010 J jnl
Preface.
Fundam. Informaticae
Thorsten Altenkirch, Tarmo Uustalu
2010 B conf
Subtyping, Declaratively.
MPC
Nils Anders Danielsson, Thorsten Altenkirch
2010 — conf
Termination Checking in the Presence of Nested Inductive and Coinductive Types.
PAR@ITP
Thorsten Altenkirch, Nils Anders Danielsson
2009 J jnl
A Universe of Strictly Positive Families.
Int. J. Found. Comput. Sci.
Peter Morris, Thorsten Altenkirch, Neil Ghani
2009 J jnl
Big-step normalisation.
J. Funct. Program.
Thorsten Altenkirch, James Chapman
2009 A* conf
Indexed Containers.
LICS
Thorsten Altenkirch, Peter Morris
2009 — ed.
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009
PLPV
Thorsten Altenkirch, Todd D. Millstein
2008 — conf
A Partial Type Checking Algorithm for Type: Type.
MSFP@ICALP
Andreas Abel, Thorsten Altenkirch
2008 — conf
Dependent Types for Distributed Arrays.
Trends in Functional Programming
Wouter Swierstra, Thorsten Altenkirch
2007 C conf
Beauty in the beast.
Haskell
Wouter Swierstra, Thorsten Altenkirch
2007 — conf
Constructing Strictly Positive Families.
CATS
Peter Morris, Thorsten Altenkirch, Neil Ghani
2007 — conf
Observational equality, now!
PLPV
Thorsten Altenkirch, Conor McBride, Wouter Swierstra
2007 — ed.
Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers
TYPES
Thorsten Altenkirch, Conor McBride
2006 — conf
From Reversible to Irreversible Computations.
QPL
Alexander S. Green, Thorsten Altenkirch
2006 — conf
Generic Programming with Dependent Types.
SSDGP
Thorsten Altenkirch, Conor McBride, Peter Morris
2006 J jnl
Structuring quantum effects: superoperators as arrows.
Math. Struct. Comput. Sci.
Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry
2006 — conf
Tait in One Big Step.
MSFP@MPC
Thorsten Altenkirch, James Chapman
2005 A* conf
A Functional Quantum Programming Language.
LICS
Thorsten Altenkirch, Jonathan Grattage
2005 — conf
An Algebra of Pure Quantum Programming.
QPL
Thorsten Altenkirch, Jonathan Grattage, Juliana Kaizer Vizzotto, Amr Sabry
2005 J jnl
Containers: Constructing strictly positive types.
Theor. Comput. Sci.
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
2005 — conf
Epigram reloaded: a standalone typechecker for ETT.
Trends in Functional Programming
James Chapman, Thorsten Altenkirch, Conor McBride
2005 J jnl
Structuring quantum effects: superoperators as arrows
CoRR
Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry
2005 J jnl
for Data: Differentiating Data Structures.
Fundam. Informaticae
Michael Gordon Abbott, Thorsten Altenkirch, Conor McBride, Neil Ghani
2004 — conf
04381 Abstracts Collection - Dependently Typed Programming.
Dependently Typed Programming
Thorsten Altenkirch, Martin Hofmann, John Hughes
2004 B conf
Constructing Polymorphic Programs with Quotient Types.
MPC
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
2004 — ed.
Dependently Typed Programming, 12.09. - 17.09.2004
Dependently Typed Programming
Thorsten Altenkirch, Martin Hofmann, John Hughes
2004 — conf
Exploring the Regular Tree Types.
TYPES
Peter Morris, Thorsten Altenkirch, Conor McBride
2004 Misc conf
Normalization by Evaluation for lambda
FLOPS
Thorsten Altenkirch, Tarmo Uustalu
2004 A* conf
Representing Nested Inductive Types Using W-Types.
ICALP
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
2003 B conf
Categories of Containers.
FoSSaCS
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
2003 — conf
Derivatives of Containers.
TLCA
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
2002 J jnl
A predicative analysis of structural recursion.
J. Funct. Program.
Andreas Abel, Thorsten Altenkirch
2002 — conf
Generic Programming within Dependently Typed Programming.
Generic Programming
Thorsten Altenkirch, Conor McBride
2001 — conf
A Finitary Subsystem of the Polymorphic lambda-Calculus.
TLCA
Thorsten Altenkirch, Thierry Coquand
2001 A* conf
Normalization by Evaluation for Typed Lambda Calculus with Coproducts.
LICS
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
2001 — conf
Representations of First Order Function Types as Terminal Coalgebras.
TLCA
Thorsten Altenkirch
2001 — conf
When is a function a fold or an unfold?
CMCS
Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch
1999 — conf
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
TYPES
Andreas Abel, Thorsten Altenkirch
1999 A* conf
Extensional Equality in Intensional Type Theory.
LICS
Thorsten Altenkirch
1999 B conf
Monadic Presentations of Lambda Terms Using Generalized Inductive Types.
CSL
Thorsten Altenkirch, Bernhard Reus
1999 — ed.
Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
TYPES
Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus
1998 B conf
Logical Relations and Inductive/Coinductive Types.
CSL
Thorsten Altenkirch
1996 — conf
Reduction-Free Normalisation for a Polymorphic System.
ISTCS
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1996 A* conf
Reduction-Free Normalisation for a Polymorphic System.
LICS
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1995 — conf
Categorical Reconstruction of a Reduction Free Normalization Proof.
Category Theory and Computer Science
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
1993 — conf
A Formalization of the Strong Normalization Proof for System F in LEGO.
TLCA
Thorsten Altenkirch
1993 — —
Constructions, inductive types and strong normalization.
Thorsten Altenkirch
1993 — conf
Proving Strong Normalization of CC by Modifying Realizability Semantics.
TYPES
Thorsten Altenkirch