Skip to content

Thorsten Altenkirch

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

32

Venues

13

Active years

1996–2026

Best venue rank

A*

Where they publish

Papers

32 indexed papers, newest first.

YearVenueTitleAuthors
2026CSLThe Groupoid-Syntax of Type Theory Is a Set.Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
2025ITPFormalising Inductive and Coinductive Containers.Stefania Damato, Thorsten Altenkirch, Axel Ljungstrm
2023FSCDCombinatory Logic and Lambda Calculus Are Equal, Algebraically.Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tams Vgh
2021FOSSACSConstructing a universe for the setoid model.Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini
2020LICSThe Integers as a Higher Inductive Type.Thorsten Altenkirch, Luis Scoccola
2019MPCSetoid Type Theory - A Syntactic Translation.Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
2018FOSSACSQuotient Inductive-Inductive Types.Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg
2018LICSFree Higher Groups in Homotopy Type Theory.Nicolai Kraus, Thorsten Altenkirch
2017FOSSACSPartiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
2016CSLExtending Homotopy Type Theory with Strict Equality.Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
2016POPLType theory in type theory using quotient inductive types.Thorsten Altenkirch, Ambrus Kaposi
2012CSLA Syntactical Approach to Weak omega-Groupoids.Thorsten Altenkirch, Ondrej Rypacek
2011CALCOA Categorical Semantics for Inductive-Inductive Definitions.Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer
2010CiEHigher-Order Containers.Thorsten Altenkirch, Paul Blain Levy, Sam Staton
2010FLOPSPiSigma: Dependent Types without the Sugar.Thorsten Altenkirch, Nils Anders Danielsson, Andres Lh, Nicolas Oury
2010FOSSACSMonads Need Not Be Endofunctors.Thorsten Altenkirch, James Chapman, Tarmo Uustalu
2010ICFPHereditary Substitutions for Simple Types, Formalized.Chantal Keller, Thorsten Altenkirch
2010ITPTermination Checking in the Presence of Nested Inductive and Coinductive Types.Thorsten Altenkirch, Nils Anders Danielsson
2010MPCSubtyping, Declaratively.Nils Anders Danielsson, Thorsten Altenkirch
2009LICSIndexed Containers.Thorsten Altenkirch, Peter Morris
2007HASKELLBeauty in the beast.Wouter Swierstra, Thorsten Altenkirch
2006MPCTait in One Big Step.Thorsten Altenkirch, James Chapman
2005LICSA Functional Quantum Programming Language.Thorsten Altenkirch, Jonathan Grattage
2004FLOPSNormalization by Evaluation for lambdaThorsten Altenkirch, Tarmo Uustalu
2004ICALPRepresenting Nested Inductive Types Using W-Types.Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
2004MPCConstructing Polymorphic Programs with Quotient Types.Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
2003FOSSACSCategories of Containers.Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
2001LICSNormalization by Evaluation for Typed Lambda Calculus with Coproducts.Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
1999CSLMonadic Presentations of Lambda Terms Using Generalized Inductive Types.Thorsten Altenkirch, Bernhard Reus
1999LICSExtensional Equality in Intensional Type Theory.Thorsten Altenkirch
1998CSLLogical Relations and Inductive/Coinductive Types.Thorsten Altenkirch
1996LICSReduction-Free Normalisation for a Polymorphic System.Thorsten Altenkirch, Martin Hofmann, Thomas Streicher