default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDThorsten Altenkirch
Person information
- affiliation: University of Nottingham, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j17]Thorsten Altenkirch
, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman:
Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8(POPL): 2340-2369 (2024)- [i12]Stefania Damato, Thorsten Altenkirch, Axel Ljungström:
Formalising inductive and coinductive containers. CoRR abs/2409.02603 (2024) - [i11]Thorsten Altenkirch, Jacob Neumann:
Synthetic 1-Categories in Directed Type Theory. CoRR abs/2410.19520 (2024) - 2023
- [c57]Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh:
Combinatory Logic and Lambda Calculus Are Equal, Algebraically. FSCD 2023: 24:1-24:19 - [i10]Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman:
Internal parametricity, without an interval. CoRR abs/2307.06448 (2023) - 2022
- [c56]Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh:
The Münchhausen Method in Type Theory. TYPES 2022: 10:1-10:20 - 2021
- [j16]Thorsten Altenkirch:
Martin Hofmann's contributions to type theory: Groupoids and univalence. Math. Struct. Comput. Sci. 31(9): 953-957 (2021) - [c55]Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini:
Constructing a universe for the setoid model. FoSSaCS 2021: 1-21 - [e6]Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch:
26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy. LIPIcs 188, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021, ISBN 978-3-95977-182-5 [contents] - [i9]Thorsten Altenkirch:
Should Type Theory replace Set Theory as the Foundation of Mathematics. CoRR abs/2111.06368 (2021) - 2020
- [c54]Thorsten Altenkirch, Luis Scoccola:
The Integers as a Higher Inductive Type. LICS 2020: 67-73 - [i8]Thorsten Altenkirch, Luis Scoccola:
The Integers as a Higher Inductive Type. CoRR abs/2007.00167 (2020)
2010 – 2019
- 2019
- [j15]Thorsten Altenkirch, Aleksy Schubert:
Preface. Fundam. Informaticae 170(1-3): v-vi (2019) - [j14]Ambrus Kaposi, András Kovács, Thorsten Altenkirch:
Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL): 2:1-2:24 (2019) - [c53]Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau:
Setoid Type Theory - A Syntactic Translation. MPC 2019: 155-196 - [c52]Thorsten Altenkirch, Colin Geniet:
Big Step Normalisation for Type Theory. TYPES 2019: 4:1-4:20 - 2018
- [c51]Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg:
Quotient Inductive-Inductive Types. FoSSaCS 2018: 293-310 - [c50]Jonathan Thaler, Thorsten Altenkirch, Peer-Olaf Siebers:
Pure Functional Epidemics: An Agent-Based Approach. IFL 2018: 1-12 - [c49]Nicolai Kraus, Thorsten Altenkirch:
Free Higher Groups in Homotopy Type Theory. LICS 2018: 599-608 - [i7]Nicolai Kraus, Thorsten Altenkirch:
Free Higher Groups in Homotopy Type Theory. CoRR abs/1805.02069 (2018) - 2017
- [j13]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) - [j12]Thorsten Altenkirch, Ambrus Kaposi:
Normalisation by Evaluation for Type Theory, in Type Theory. Log. Methods Comput. Sci. 13(4) (2017) - [c48]Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus:
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. FoSSaCS 2017: 534-549 - 2016
- [j11]Thorsten Altenkirch, Conor McBride:
Selected papers from Dependently Typed Programming 2010 - Overview. Math. Struct. Comput. Sci. 26(1): 1-2 (2016) - [c47]Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus:
Extending Homotopy Type Theory with Strict Equality. CSL 2016: 21:1-21:17 - [c46]Thorsten Altenkirch, Ambrus Kaposi:
Type theory in type theory using quotient inductive types. POPL 2016: 18-29 - [c45]Thorsten Altenkirch, Ambrus Kaposi:
Normalisation by Evaluation for Dependent Types. FSCD 2016: 6:1-6:16 - [i6]Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus:
Extending Homotopy Type Theory with Strict Equality. CoRR abs/1604.03799 (2016) - [i5]Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus:
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. CoRR abs/1610.09254 (2016) - [i4]Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg:
Quotient inductive-inductive types. CoRR abs/1612.02346 (2016) - [i3]Thorsten Altenkirch, Ambrus Kaposi:
Normalisation by Evaluation for Type Theory, in Type Theory. CoRR abs/1612.02462 (2016) - 2015
- [j10]Thorsten Altenkirch, James Chapman, Tarmo Uustalu:
Monads need not be endofunctors. Log. Methods Comput. Sci. 11(1) (2015) - [j9]Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, Peter Morris:
Indexed containers. J. Funct. Program. 25 (2015) - [c44]Thorsten Altenkirch, Ambrus Kaposi:
Towards a Cubical Type Theory without an Interval. TYPES 2015: 3:1-3:27 - [e5]Thorsten Altenkirch:
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland. LIPIcs 38, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2015, ISBN 978-3-939897-87-3 [contents] - 2014
- [j8]Thorsten Altenkirch, James Chapman, Tarmo Uustalu:
Relative Monads Formalised. J. Formaliz. Reason. 7(1): 1-43 (2014) - [c43]Thorsten Altenkirch, Nuo Li, Ondrej Rypacek:
Some constructions on ω-groupoids. LFMTP 2014: 4: 1-4: 8 - 2013
- [c42]Peter G. Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch:
Small Induction Recursion. TLCA 2013: 156-172 - [c41]Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch:
Generalizations of Hedberg's Theorem. TLCA 2013: 173-188 - 2012
- [c40]Thorsten Altenkirch, Ondrej Rypacek:
A Syntactical Approach to Weak omega-Groupoids. CSL 2012: 16-30 - 2011
- [c39]Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer:
A Categorical Semantics for Inductive-Inductive Definitions. CALCO 2011: 70-84 - 2010
- [j7]Thorsten Altenkirch, Tarmo Uustalu:
Preface. Fundam. Informaticae 102(2) (2010) - [c38]Thorsten Altenkirch, Paul Blain Levy, Sam Staton:
Higher-Order Containers. CiE 2010: 11-20 - [c37]Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury:
PiSigma: Dependent Types without the Sugar. FLOPS 2010: 40-55 - [c36]Thorsten Altenkirch, James Chapman, Tarmo Uustalu:
Monads Need Not Be Endofunctors. FoSSaCS 2010: 297-311 - [c35]Chantal Keller, Thorsten Altenkirch:
Hereditary Substitutions for Simple Types, Formalized. MSFP@ICFP 2010: 3-10 - [c34]Thorsten Altenkirch, Nils Anders Danielsson:
Termination Checking in the Presence of Nested Inductive and Coinductive Types. PAR@ITP 2010: 101-106 - [c33]Nils Anders Danielsson, Thorsten Altenkirch:
Subtyping, Declaratively. MPC 2010: 100-118
2000 – 2009
- 2009
- [j6]Peter Morris, Thorsten Altenkirch, Neil Ghani:
A Universe of Strictly Positive Families. Int. J. Found. Comput. Sci. 20(1): 83-107 (2009) - [j5]Thorsten Altenkirch, James Chapman:
Big-step normalisation. J. Funct. Program. 19(3-4): 311-333 (2009) - [c32]Thorsten Altenkirch, Peter Morris:
Indexed Containers. LICS 2009: 277-285 - [e4]Thorsten Altenkirch, Todd D. Millstein:
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009. ACM 2009, ISBN 978-1-60558-330-3 [contents] - 2008
- [c31]Wouter Swierstra, Thorsten Altenkirch:
Dependent Types for Distributed Arrays. Trends in Functional Programming 2008: 17-32 - [c30]Andreas Abel, Thorsten Altenkirch:
A Partial Type Checking Algorithm for Type: Type. MSFP@ICALP 2008: 3-17 - 2007
- [c29]Peter Morris, Thorsten Altenkirch, Neil Ghani:
Constructing Strictly Positive Families. CATS 2007: 111-121 - [c28]Wouter Swierstra, Thorsten Altenkirch:
Beauty in the beast. Haskell 2007: 25-36 - [c27]Thorsten Altenkirch, Conor McBride, Wouter Swierstra:
Observational equality, now! PLPV 2007: 57-68 - [e3]Thorsten Altenkirch, Conor McBride:
Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Lecture Notes in Computer Science 4502, Springer 2007, ISBN 978-3-540-74463-4 [contents] - 2006
- [j4]Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry:
Structuring quantum effects: superoperators as arrows. Math. Struct. Comput. Sci. 16(3): 453-468 (2006) - [c26]Thorsten Altenkirch, James Chapman:
Tait in One Big Step. MSFP@MPC 2006 - [c25]Thorsten Altenkirch, Conor McBride, Peter Morris:
Generic Programming with Dependent Types. SSDGP 2006: 209-257 - [c24]Alexander S. Green, Thorsten Altenkirch:
From Reversible to Irreversible Computations. QPL 2006: 65-74 - 2005
- [j3]Michael Gordon Abbott, Thorsten Altenkirch, Conor McBride, Neil Ghani:
for Data: Differentiating Data Structures. Fundam. Informaticae 65(1-2): 1-28 (2005) - [j2]Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani:
Containers: Constructing strictly positive types. Theor. Comput. Sci. 342(1): 3-27 (2005) - [c23]Thorsten Altenkirch, Jonathan Grattage:
A Functional Quantum Programming Language. LICS 2005: 249-258 - [c22]James Chapman, Thorsten Altenkirch, Conor McBride:
Epigram reloaded: a standalone typechecker for ETT. Trends in Functional Programming 2005: 79-94 - [c21]Thorsten Altenkirch, Jonathan Grattage, Juliana Kaizer Vizzotto, Amr Sabry:
An Algebra of Pure Quantum Programming. QPL 2005: 23-47 - [i2]Juliana Kaizer Vizzotto, Thorsten Altenkirch, Amr Sabry:
Structuring quantum effects: superoperators as arrows. CoRR abs/quant-ph/0501151 (2005) - 2004
- [c20]Thorsten Altenkirch, Tarmo Uustalu:
Normalization by Evaluation for lambda-2. FLOPS 2004: 260-275 - [c19]Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani:
Representing Nested Inductive Types Using W-Types. ICALP 2004: 59-71 - [c18]Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride:
Constructing Polymorphic Programs with Quotient Types. MPC 2004: 2-15 - [c17]Peter Morris, Thorsten Altenkirch, Conor McBride:
Exploring the Regular Tree Types. TYPES 2004: 252-267 - [e2]Thorsten Altenkirch, Martin Hofmann, John Hughes:
Dependently Typed Programming, 12.09. - 17.09.2004. Dagstuhl Seminar Proceedings 04381, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2004 [contents] - [i1]Thorsten Altenkirch, Martin Hofmann, John Hughes:
04381 Abstracts Collection - Dependently Typed Programming. Dependently Typed Programming 2004 - 2003
- [c16]Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani:
Categories of Containers. FoSSaCS 2003: 23-38 - [c15]Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride:
Derivatives of Containers. TLCA 2003: 16-30 - 2002
- [j1]Andreas Abel, Thorsten Altenkirch:
A predicative analysis of structural recursion. J. Funct. Program. 12(1): 1-41 (2002) - [c14]Thorsten Altenkirch, Conor McBride:
Generic Programming within Dependently Typed Programming. Generic Programming 2002: 1-20 - 2001
- [c13]Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott:
Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS 2001: 303-310 - [c12]Thorsten Altenkirch:
Representations of First Order Function Types as Terminal Coalgebras. TLCA 2001: 8-21 - [c11]Thorsten Altenkirch, Thierry Coquand:
A Finitary Subsystem of the Polymorphic lambda-Calculus. TLCA 2001: 22-28 - [c10]Jeremy Gibbons, Graham Hutton, Thorsten Altenkirch:
When is a function a fold or an unfold? CMCS 2001: 146-160
1990 – 1999
- 1999
- [c9]Thorsten Altenkirch, Bernhard Reus:
Monadic Presentations of Lambda Terms Using Generalized Inductive Types. CSL 1999: 453-468 - [c8]Thorsten Altenkirch:
Extensional Equality in Intensional Type Theory. LICS 1999: 412-420 - [c7]Andreas Abel, Thorsten Altenkirch:
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types. TYPES 1999: 21-40 - [e1]Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus:
Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers. Lecture Notes in Computer Science 1657, Springer 1999, ISBN 3-540-66537-4 [contents] - 1998
- [c6]Thorsten Altenkirch:
Logical Relations and Inductive/Coinductive Types. CSL 1998: 343-354 - 1996
- [c5]Thorsten Altenkirch, Martin Hofmann, Thomas Streicher:
Reduction-Free Normalisation for a Polymorphic System. ISTCS 1996: 146 - [c4]Thorsten Altenkirch, Martin Hofmann, Thomas Streicher:
Reduction-Free Normalisation for a Polymorphic System. LICS 1996: 98-106 - 1995
- [c3]Thorsten Altenkirch, Martin Hofmann, Thomas Streicher:
Categorical Reconstruction of a Reduction Free Normalization Proof. Category Theory and Computer Science 1995: 182-199 - 1993
- [b1]Thorsten Altenkirch:
Constructions, inductive types and strong normalization. University of Edinburgh, UK, CST 106, 1993, pp. 1-183 - [c2]Thorsten Altenkirch:
A Formalization of the Strong Normalization Proof for System F in LEGO. TLCA 1993: 13-28 - [c1]Thorsten Altenkirch:
Proving Strong Normalization of CC by Modifying Realizability Semantics. TYPES 1993: 3-18
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-01 00:13 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
