Thorsten Altenkirch

ORCID

Publication Activity (10 Years)

Years Active: 1993-2024
Publications (10 Years): 28

Top Venues

CoRR

FoSSaCS

TYPES

Log. Methods Comput. Sci.

University of Edinburgh, UK (PHD)

Education History

University of Edinburgh, UK

PHD

Publications

Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8 (POPL) (2024)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
Combinatory Logic and Lambda Calculus Are Equal, Algebraically. FSCD (2023)
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
Internal parametricity, without an interval. CoRR (2023)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
The Münchhausen Method in Type Theory. TYPES (2022)
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini
Constructing a universe for the setoid model. FoSSaCS (2021)
Thorsten Altenkirch
Should Type Theory replace Set Theory as the Foundation of Mathematics. CoRR (2021)
Thorsten Altenkirch
Martin Hofmann's contributions to type theory: Groupoids and univalence. Math. Struct. Comput. Sci. 31 (9) (2021)
Thorsten Altenkirch, Luis Scoccola
The Integers as a Higher Inductive Type. LICS (2020)
Thorsten Altenkirch, Luis Scoccola
The Integers as a Higher Inductive Type. CoRR (2020)
Ambrus Kaposi, András Kovács, Thorsten Altenkirch
Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3 (POPL) (2019)
Thorsten Altenkirch, Colin Geniet
Big Step Normalisation for Type Theory. TYPES (2019)
Thorsten Altenkirch, Aleksy Schubert
Preface. Fundam. Informaticae 170 (1-3) (2019)
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
Setoid Type Theory - A Syntactic Translation. MPC (2019)
Nicolai Kraus, Thorsten Altenkirch
Free Higher Groups in Homotopy Type Theory. LICS (2018)
Jonathan Thaler, Thorsten Altenkirch, Peer-Olaf Siebers
Pure Functional Epidemics: An Agent-Based Approach. IFL (2018)
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg
Quotient Inductive-Inductive Types. FoSSaCS (2018)
Nicolai Kraus, Thorsten Altenkirch
Free Higher Groups in Homotopy Type Theory. CoRR (2018)
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. FoSSaCS (2017)
Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
Notions of Anonymous Existence in Martin-Löf Type Theory. Log. Methods Comput. Sci. 13 (1) (2017)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Type Theory, in Type Theory. Log. Methods Comput. Sci. 13 (4) (2017)
Thorsten Altenkirch, Ambrus Kaposi
Type theory in type theory using quotient inductive types. POPL (2016)
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Extending Homotopy Type Theory with Strict Equality. CSL (2016)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Type Theory, in Type Theory. CoRR (2016)
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Extending Homotopy Type Theory with Strict Equality. CoRR (2016)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Dependent Types. FSCD (2016)
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg
Quotient inductive-inductive types. CoRR (2016)
Thorsten Altenkirch, Conor McBride
Selected papers from Dependently Typed Programming 2010 - Overview. Math. Struct. Comput. Sci. 26 (1) (2016)
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. CoRR (2016)
Thorsten Altenkirch, Ambrus Kaposi
Towards a Cubical Type Theory without an Interval. TYPES (2015)
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
Monads need not be endofunctors. Log. Methods Comput. Sci. 11 (1) (2015)
Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, Peter Morris
Indexed containers. J. Funct. Program. 25 (2015)
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
Relative Monads Formalised. J. Formaliz. Reason. 7 (1) (2014)
Thorsten Altenkirch, Nuo Li, Ondrej Rypacek
Some constructions on ω-groupoids. LFMTP (2014)
Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch
Generalizations of Hedberg's Theorem. TLCA (2013)
Peter G. Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch
Small Induction Recursion. TLCA (2013)
Thorsten Altenkirch, Ondrej Rypacek
A Syntactical Approach to Weak omega-Groupoids. CSL (2012)
Andreas Abel, Thorsten Altenkirch
A Partial Type Checking Algorithm for Type: Type. Electron. Notes Theor. Comput. Sci. 229 (5) (2011)
Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer
A Categorical Semantics for Inductive-Inductive Definitions. CALCO (2011)
Nils Anders Danielsson, Thorsten Altenkirch
Subtyping, Declaratively. MPC (2010)
Thorsten Altenkirch, James Chapman, Tarmo Uustalu
Monads Need Not Be Endofunctors. FoSSaCS (2010)
Thorsten Altenkirch, Nils Anders Danielsson
Termination Checking in the Presence of Nested Inductive and Coinductive Types. PAR@ITP (2010)
Chantal Keller, Thorsten Altenkirch
Hereditary Substitutions for Simple Types, Formalized. MSFP@ICFP (2010)
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury
PiSigma: Dependent Types without the Sugar. FLOPS (2010)
Thorsten Altenkirch, Tarmo Uustalu
Preface. Fundam. Informaticae 102 (2) (2010)
Thorsten Altenkirch, Paul Blain Levy, Sam Staton
Higher-Order Containers. CiE (2010)
Peter Morris, Thorsten Altenkirch, Neil Ghani
A Universe of Strictly Positive Families. Int. J. Found. Comput. Sci. 20 (1) (2009)
Thorsten Altenkirch, James Chapman
Big-step normalisation. J. Funct. Program. 19 (3-4) (2009)
Thorsten Altenkirch, Peter Morris
Indexed Containers. LICS (2009)
Alexander S. Green, Thorsten Altenkirch
From Reversible to Irreversible Computations. Electron. Notes Theor. Comput. Sci. 210 (2008)
Wouter Swierstra, Thorsten Altenkirch
Dependent Types for Distributed Arrays. Trends in Functional Programming (2008)
Peter Morris, Thorsten Altenkirch, Neil Ghani
Constructing Strictly Positive Families. CATS (2007)
Thorsten Altenkirch, Conor McBride, Wouter Swierstra
Observational equality, now! PLPV (2007)
Wouter Swierstra, Thorsten Altenkirch
Beauty in the beast. Haskell (2007)
Thorsten Altenkirch, Jonathan Grattage, Juliana Kaizer Vizzotto, Amr Sabry
An Algebra of Pure Quantum Programming. Electron. Notes Theor. Comput. Sci. 170 (2007)
Thorsten Altenkirch, James Chapman
Tait in One Big Step. MSFP@MPC (2006)
Thorsten Altenkirch, Conor McBride, Peter Morris
Generic Programming with Dependent Types. SSDGP (2006)
Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry
Structuring quantum effects: superoperators as arrows. Math. Struct. Comput. Sci. 16 (3) (2006)
Thorsten Altenkirch, Jonathan Grattage
A Functional Quantum Programming Language. LICS (2005)
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
Containers: Constructing strictly positive types. Theor. Comput. Sci. 342 (1) (2005)
Michael Gordon Abbott, Thorsten Altenkirch, Conor McBride, Neil Ghani
for Data: Differentiating Data Structures. Fundam. Informaticae 65 (1-2) (2005)
Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry
Structuring quantum effects: superoperators as arrows CoRR (2005)
James Chapman, Thorsten Altenkirch, Conor McBride
Epigram reloaded: a standalone typechecker for ETT. Trends in Functional Programming (2005)
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
Constructing Polymorphic Programs with Quotient Types. MPC (2004)
Peter Morris, Thorsten Altenkirch, Conor McBride
Exploring the Regular Tree Types. TYPES (2004)
Thorsten Altenkirch, Martin Hofmann, John Hughes
04381 Abstracts Collection - Dependently Typed Programming. Dependently Typed Programming (2004)
Thorsten Altenkirch, Tarmo Uustalu
. FLOPS (2004)
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
Representing Nested Inductive Types Using W-Types. ICALP (2004)
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
Derivatives of Containers. TLCA (2003)
Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani
Categories of Containers. FoSSaCS (2003)
Andreas Abel, Thorsten Altenkirch
A predicative analysis of structural recursion. J. Funct. Program. 12 (1) (2002)
Thorsten Altenkirch, Conor McBride
Generic Programming within Dependently Typed Programming. Generic Programming (2002)
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS (2001)
Thorsten Altenkirch
Representations of First Order Function Types as Terminal Coalgebras. TLCA (2001)
Thorsten Altenkirch, Thierry Coquand
A Finitary Subsystem of the Polymorphic lambda-Calculus. TLCA (2001)
Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch
When is a function a fold or an unfold? CMCS (2001)
Andreas Abel, Thorsten Altenkirch
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. TYPES (1999)
Thorsten Altenkirch
Extensional Equality in Intensional Type Theory. LICS (1999)
Thorsten Altenkirch, Bernhard Reus
Monadic Presentations of Lambda Terms Using Generalized Inductive Types. CSL (1999)
Thorsten Altenkirch
Logical Relations and Inductive/Coinductive Types. CSL (1998)
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
Reduction-Free Normalisation for a Polymorphic System. LICS (1996)
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
Reduction-Free Normalisation for a Polymorphic System. ISTCS (1996)
Thorsten Altenkirch, Martin Hofmann, Thomas Streicher
Categorical Reconstruction of a Reduction Free Normalization Proof. Category Theory and Computer Science (1995)
Thorsten Altenkirch
A Formalization of the Strong Normalization Proof for System F in LEGO. TLCA (1993)
Thorsten Altenkirch
Proving Strong Normalization of CC by Modifying Realizability Semantics. TYPES (1993)

Thorsten Altenkirch.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Thorsten Altenkirch