Constructions, inductive types and strong normalization. - Thorsten Altenkirch (1993)

A Formalization of the Strong Normalization Proof for System F in LEGO. - Thorsten Altenkirch (TLCA, 1993)

Proving Strong Normalization of CC by Modifying Realizability Semantics. - Thorsten Altenkirch (TYPES, 1993)

Categorical Reconstruction of a Reduction Free Normalization Proof. - Thorsten Altenkirch; Martin Hofmann 001; Thomas Streicher (Category Theory and Computer Science, 1995)

Reduction-Free Normalisation for a Polymorphic System. - Thorsten Altenkirch; Martin Hofmann 001; Thomas Streicher (ISTCS, 1996)

Logical Relations and Inductive/Coinductive Types. - Thorsten Altenkirch (CSL, 1998)

Monadic Presentations of Lambda Terms Using Generalized Inductive Types. - Thorsten Altenkirch; Bernhard Reus (CSL, 1999)

Extensional Equality in Intensional Type Theory. - Thorsten Altenkirch (LICS, 1999)

A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. - Andreas Abel 001; Thorsten Altenkirch (TYPES, 1999)

Normalization by Evaluation for Typed Lambda Calculus with Coproducts. - Thorsten Altenkirch; Peter Dybjer; Martin Hofmann 001; Philip J. Scott (LICS, 2001)

Representations of First Order Function Types as Terminal Coalgebras. - Thorsten Altenkirch (TLCA, 2001)

A Finitary Subsystem of the Polymorphic lambda-Calculus. - Thorsten Altenkirch; Thierry Coquand (TLCA, 2001)

When is a function a fold or an unfold? - Jeremy Gibbons; Graham Hutton; Thorsten Altenkirch (CMCS, 2001)

Generic Programming within Dependently Typed Programming. - Thorsten Altenkirch; Conor McBride (Generic Programming, 2002)

A predicative analysis of structural recursion. - Andreas Abel 001; Thorsten Altenkirch (J. Funct. Program., 2002)

Categories of Containers. - Michael Gordon Abbott; Thorsten Altenkirch; Neil Ghani (FoSSaCS, 2003)

Derivatives of Containers. - Michael Gordon Abbott; Thorsten Altenkirch; Neil Ghani; Conor McBride (TLCA, 2003)

04381 Abstracts Collection - Dependently Typed Programming. - Thorsten Altenkirch; Martin Hofmann 001; John Hughes 001 (Dependently Typed Programming, 2004)

Normalization by Evaluation for lambda-2. - Thorsten Altenkirch; Tarmo Uustalu (FLOPS, 2004)

Representing Nested Inductive Types Using W-Types. - Michael Gordon Abbott; Thorsten Altenkirch; Neil Ghani (ICALP, 2004)

Constructing Polymorphic Programs with Quotient Types. - Michael Gordon Abbott; Thorsten Altenkirch; Neil Ghani; Conor McBride (MPC, 2004)

Exploring the Regular Tree Types. - Peter Morris; Thorsten Altenkirch; Conor McBride (TYPES, 2004)

A Functional Quantum Programming Language. - Thorsten Altenkirch; Jonathan Grattage (LICS, 2005)

Epigram reloaded: a standalone typechecker for ETT. - James Chapman 001; Thorsten Altenkirch; Conor McBride (Trends in Functional Programming, 2005)

An Algebra of Pure Quantum Programming. - Thorsten Altenkirch; Jonathan Grattage; Juliana Kaizer Vizzotto; Amr Sabry (QPL, 2005)

for Data: Differentiating Data Structures. - Michael Gordon Abbott; Thorsten Altenkirch; Conor McBride; Neil Ghani (Fundam. Informaticae, 2005)

Containers: Constructing strictly positive types. - Michael Gordon Abbott; Thorsten Altenkirch; Neil Ghani (Theor. Comput. Sci., 2005)

Tait in One Big Step. - Thorsten Altenkirch; James Chapman 001 (MSFP@MPC, 2006)

Generic Programming with Dependent Types. - Thorsten Altenkirch; Conor McBride; Peter Morris (SSDGP, 2006)

From Reversible to Irreversible Computations. - Alexander S. Green; Thorsten Altenkirch (QPL, 2006)

Structuring quantum effects: superoperators as arrows. - Juliana Kaizer Vizzotto; Thorsten Altenkirch; Amr Sabry (Math. Struct. Comput. Sci., 2006)

Constructing Strictly Positive Families. - Peter Morris; Thorsten Altenkirch; Neil Ghani (CATS, 2007)

Beauty in the beast. - Wouter Swierstra; Thorsten Altenkirch (Haskell, 2007)

Observational equality, now! - Thorsten Altenkirch; Conor McBride; Wouter Swierstra (PLPV, 2007)

Dependent Types for Distributed Arrays. - Wouter Swierstra; Thorsten Altenkirch (Trends in Functional Programming, 2008)

A Partial Type Checking Algorithm for Type: Type. - Andreas Abel 001; Thorsten Altenkirch (MSFP@ICALP, 2008)

Indexed Containers. - Thorsten Altenkirch; Peter Morris (LICS, 2009)

A Universe of Strictly Positive Families. - Peter Morris; Thorsten Altenkirch; Neil Ghani (Int. J. Found. Comput. Sci., 2009)

Big-step normalisation. - Thorsten Altenkirch; James Chapman 001 (J. Funct. Program., 2009)

Higher-Order Containers. - Thorsten Altenkirch; Paul Blain Levy; Sam Staton (CiE, 2010)

PiSigma: Dependent Types without the Sugar. - Thorsten Altenkirch; Nils Anders Danielsson; Andres Löh; Nicolas Oury (FLOPS, 2010)

Hereditary Substitutions for Simple Types, Formalized. - Chantal Keller; Thorsten Altenkirch (MSFP@ICFP, 2010)

Termination Checking in the Presence of Nested Inductive and Coinductive Types. - Thorsten Altenkirch; Nils Anders Danielsson (PAR@ITP, 2010)

Subtyping, Declaratively. - Nils Anders Danielsson; Thorsten Altenkirch (MPC, 2010)

Preface. - Thorsten Altenkirch; Tarmo Uustalu (Fundam. Informaticae, 2010)

A Categorical Semantics for Inductive-Inductive Definitions. - Thorsten Altenkirch; Peter Morris; Fredrik Nordvall Forsberg; Anton Setzer (CALCO, 2011)

A Syntactical Approach to Weak omega-Groupoids. - Thorsten Altenkirch; Ondrej Rypacek (CSL, 2012)

Small Induction Recursion. - Peter G. Hancock; Conor McBride; Neil Ghani; Lorenzo Malatesta; Thorsten Altenkirch (TLCA, 2013)

Generalizations of Hedberg's Theorem. - Nicolai Kraus; Martín Hötzel Escardó; Thierry Coquand; Thorsten Altenkirch (TLCA, 2013)

Some constructions on ω-groupoids. - Thorsten Altenkirch; Nuo Li; Ondrej Rypacek (LFMTP, 2014)

Relative Monads Formalised. - Thorsten Altenkirch; James Chapman 001; Tarmo Uustalu (J. Formaliz. Reason., 2014)

Towards a Cubical Type Theory without an Interval. - Thorsten Altenkirch; Ambrus Kaposi (TYPES, 2015)

Monads need not be endofunctors. - Thorsten Altenkirch; James Chapman 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2015)

Indexed containers. - Thorsten Altenkirch; Neil Ghani; Peter G. Hancock; Conor McBride; Peter Morris (J. Funct. Program., 2015)

Extending Homotopy Type Theory with Strict Equality. - Thorsten Altenkirch; Paolo Capriotti; Nicolai Kraus (CSL, 2016)

Type theory in type theory using quotient inductive types. - Thorsten Altenkirch; Ambrus Kaposi (POPL, 2016)

Normalisation by Evaluation for Dependent Types. - Thorsten Altenkirch; Ambrus Kaposi (FSCD, 2016)

Quotient inductive-inductive types. - Thorsten Altenkirch; Paolo Capriotti; Gabe Dijkstra; Fredrik Nordvall Forsberg (CoRR, 2016)

Selected papers from Dependently Typed Programming 2010 - Overview. - Thorsten Altenkirch; Conor McBride (Math. Struct. Comput. Sci., 2016)

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. - Thorsten Altenkirch; Nils Anders Danielsson; Nicolai Kraus (FoSSaCS, 2017)

Notions of Anonymous Existence in Martin-Löf Type Theory. - Nicolai Kraus; Martín Escardó; Thierry Coquand; Thorsten Altenkirch (Log. Methods Comput. Sci., 2017)

Normalisation by Evaluation for Type Theory, in Type Theory. - Thorsten Altenkirch; Ambrus Kaposi (Log. Methods Comput. Sci., 2017)

Quotient Inductive-Inductive Types. - Thorsten Altenkirch; Paolo Capriotti; Gabe Dijkstra; Nicolai Kraus; Fredrik Nordvall Forsberg (FoSSaCS, 2018)

Pure Functional Epidemics: An Agent-Based Approach. - Jonathan Thaler; Thorsten Altenkirch; Peer-Olaf Siebers (IFL, 2018)

Free Higher Groups in Homotopy Type Theory. - Nicolai Kraus; Thorsten Altenkirch (LICS, 2018)

Setoid Type Theory - A Syntactic Translation. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Nicolas Tabareau (MPC, 2019)

Big Step Normalisation for Type Theory. - Thorsten Altenkirch; Colin Geniet (TYPES, 2019)

Preface. - Thorsten Altenkirch; Aleksy Schubert (Fundam. Informaticae, 2019)

Constructing quotient inductive-inductive types. - Ambrus Kaposi; András Kovács; Thorsten Altenkirch (Proc. ACM Program. Lang., 2019)

The Integers as a Higher Inductive Type. - Thorsten Altenkirch; Luis Scoccola (LICS, 2020)

Constructing a universe for the setoid model. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Christian Sattler; Filippo Sestini (FoSSaCS, 2021)

Should Type Theory replace Set Theory as the Foundation of Mathematics. - Thorsten Altenkirch (CoRR, 2021)

Martin Hofmann's contributions to type theory: Groupoids and univalence. - Thorsten Altenkirch (Math. Struct. Comput. Sci., 2021)

The Münchhausen Method in Type Theory. - Thorsten Altenkirch; Ambrus Kaposi; Artjoms Sinkarovs; Tamás Végh (TYPES, 2022)

Combinatory Logic and Lambda Calculus Are Equal, Algebraically. - Thorsten Altenkirch; Ambrus Kaposi; Artjoms Sinkarovs; Tamás Végh (FSCD, 2023)

Synthetic 1-Categories in Directed Type Theory. - Jacob Neumann; Thorsten Altenkirch (TYPES, 2024)

Formalising inductive and coinductive containers. - Stefania Damato; Thorsten Altenkirch; Axel Ljungström (CoRR, 2024)

Preface: Advances in Homotopy Type Theory. - Thorsten Altenkirch; Benno van den Berg; Nicola Gambino; Maria Emilia Maietti (Math. Struct. Comput. Sci., 2024)

Internal Parametricity, without an Interval. - Thorsten Altenkirch; Yorgo Chamoun; Ambrus Kaposi; Michael Shulman (Proc. ACM Program. Lang., 2024)