×

Altenkirch, Thorsten

Author ID: altenkirch.thorsten Recent zbMATH articles by "Altenkirch, Thorsten"
Published as: Altenkirch, Thorsten
Homepage: http://www.cs.nott.ac.uk/~psztxa/
External Links: MGP · ORCID · Wikidata · Google Scholar · ResearchGate · dblp · IdRef · theses.fr
all top 5

Co-Authors

8 single-authored
9 Ghani, Neil
9 McBride, Conor Thomas
7 Kraus, Nicolai
6 Kaposi, Ambrus
5 Uustalu, Tarmo
4 Chapman, James T. E.
4 Coquand, Thierry
4 Morris, Peter A.
3 Abel, Andreas M.
3 Danielsson, Nils Anders
3 Hötzel Escardó, Martín
2 Boulier, Simon
2 Capriotti, Paolo
2 Green, Alexander S.
2 Hancock, Peter G.
2 Hofmann, Martin
2 Nordvall Forsberg, Fredrik
2 Reus, Bernhard
2 Sabry, Amr
2 Vizzotto, Juliana Kaizer
1 Aczel, Peter
1 Ahrens, Benedikt
1 Angiuli, Carlo
1 Avigad, Jeremy
1 Awodey, Steve
1 Barras, Bruno
1 Bauer, Andrej
1 Berardi, Stefano
1 Bertot, Yves
1 Bezem, Marc
1 Bordg, Anthony
1 Brunerie, Guillaume
1 Cohen, Cyril
1 Constable, Robert Lee
1 Curien, Pierre-Louis
1 de’Liguoro, Ugo
1 Dijkstra, Gabe
1 Dybjer, Peter
1 Finster, Eric
1 Gambino, Nicola
1 Garner, Richard
1 Geniet, Colin
1 Gibbons, Jeremy
1 Gonthier, Georges
1 Grattage, Jonathan
1 Grayson, Daniel Richard
1 Hales, Thomas Callister
1 Harper, Robert
1 Herbelin, Hugo
1 Hofstra, Pieter J. W.
1 Hou (Favonia), Kuen-Bang
1 Hutton, Graham
1 Joyal, André
1 Kapulkin, Krzysztof
1 Kock, Joachim
1 Levy, Paul Blain
1 Li, Nuo
1 Licata, Dan
1 Löh, Andres
1 Lumsdaine, Peter LeFanu
1 Luo, Zhaohui
1 Mahboubi, Assia
1 Malatesta, Lorenzo
1 Martin-Löf, Per
1 Melikhov, Sergey Aleksandrovich
1 Nahas, Michael
1 Naraschewski, Wolfgang
1 Oury, Nicolas
1 Palmgren, Erik
1 Pelayo, Alvaro
1 Polonsky, Andrew
1 Riehl, Emily
1 Rijke, Egbert
1 Rypacek, Ondrej
1 Sattler, Christian
1 Schubert, Aleksy
1 Scoccola, Luis Nerio
1 Scott, Dana Stewart
1 Scott, Philip J.
1 Sestini, Filippo
1 Setzer, Anton
1 Shulman, Michael A.
1 Sojakova, Kristina
1 Solov’ëv, Sergeĭ Vladimirovich
1 Sozeau, Matthieu
1 Spitters, Bas
1 Staton, Sam
1 Streicher, Thomas
1 Tabareau, Nicolas
1
1 Urzyczyn, Paweł
1 Van den Berg, Benno
1 Voevodskiĭ, Vladimir Aleksandrovich
1 Warren, Michael Alton
1 Zeilberger, Noam

Publications by Year

Citations contained in zbMATH Open

50 Publications have been cited 408 times in 247 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
Containers: Constructing strictly positive types. Zbl 1077.68015
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
38
2005
Monadic presentations of lambda terms using generalized inductive types. Zbl 0944.03011
Altenkirch, Thorsten; Reus, Bernhard
31
1999
Categories of containers. Zbl 1029.68096
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
29
2003
Type theory in type theory using quotient inductive types. Zbl 1347.68045
Altenkirch, Thorsten; Kaposi, Ambrus
26
2016
Indexed containers. Zbl 1420.68032
Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; Mcbride, Conor; Morris, Peter
22
2015
Monads need not be endofunctors. Zbl 1448.18007
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
21
2015
A formalization of the strong normalization proof for system F in LEGO. Zbl 0797.68095
Altenkirch, Thorsten
16
1993
Monads need not be endofunctors. Zbl 1284.18010
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
16
2010
Partiality, revisited. The partiality monad as a quotient inductive-inductive type. Zbl 1486.68036
Altenkirch, Thorsten; Danielsson, Nils Anders; Kraus, Nicolai
12
2017
A predicative analysis of structural recursion. Zbl 0998.68027
Abel, Andreas; Altenkirch, Thorsten
11
2002
Quotient inductive-inductive types. Zbl 1506.03063
Altenkirch, Thorsten; Capriotti, Paolo; Dijkstra, Gabe; Kraus, Nicolai; Nordvall Forsberg, Fredrik
11
2018
Subtyping, declaratively. An exercise in mixed induction and coinduction. Zbl 1286.68074
Danielsson, Nils Anders; Altenkirch, Thorsten
10
2010
Generic programming within dependently typed programming. Zbl 1089.68529
Altenkirch, Thorsten; McBride, Conor
10
2003
Structuring quantum effects: superoperators as arrows. Zbl 1122.68062
Vizzotto, Juliana; Altenkirch, Thorsten; Sabry, Amr
9
2006
Small induction recursion. Zbl 1381.68189
Hancock, Peter; McBride, Conor; Ghani, Neil; Malatesta, Lorenzo; Altenkirch, Thorsten
9
2013
An algebra of pure quantum programming. Zbl 1277.68053
Altenkirch, Thorsten; Grattage, Jonathan; Vizzotto, Juliana K.; Sabry, Amr
9
2007
Derivatives of containers. Zbl 1039.68078
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil; McBride, Conor
9
2003
Big-step normalisation. Zbl 1191.68153
Altenkirch, Thorsten; Chapman, James
9
2009
Categorical reconstruction of a reduction free normalization proof. Zbl 1502.03019
Altenkirch, Thorsten; Hofmann, Martin; Streicher, Thomas
8
1995
Representing nested inductive types using W-types. Zbl 1099.03058
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
7
2004
Extending homotopy type theory with strict equality. Zbl 1370.03014
Altenkirch, Thorsten; Capriotti, Paolo; Kraus, Nicolai
7
2016
Normalisation by evaluation for type theory, in type theory. Zbl 1459.03013
Altenkirch, Thorsten; Kaposi, Ambrus
7
2017
\(\partial\) for data: Differentiating data structures. Zbl 1102.68020
Abbott, Michael; Altenkirch, Thorsten; McBride, Conor; Ghani, Neil
7
2005
A categorical semantics for inductive-inductive definitions. Zbl 1344.68143
Altenkirch, Thorsten; Morris, Peter; Nordvall Forsberg, Fredrik; Setzer, Anton
5
2011
A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020
Altenkirch, Thorsten; Coquand, Thierry
5
2001
Normalisation by evaluation for dependent types. Zbl 1387.68060
Altenkirch, Thorsten; Kaposi, Ambrus
5
2016
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
5
2017
Constructing polymorphic programs with quotient types. Zbl 1106.68335
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil; McBride, Conor
4
2004
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
4
2013
\(\Pi \Sigma \): dependent types without the sugar. Zbl 1284.68122
Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas
4
2010
The quantum IO monad. Zbl 1209.68103
Altenkirch, Thorsten; Green, Alexander S.
4
2010
Representations of first order function types as terminal coalgebras. Zbl 0981.68110
Altenkirch, Thorsten
4
2001
Free higher groups in homotopy type theory. Zbl 1453.03003
Kraus, Nicolai; Altenkirch, Thorsten
4
2018
A syntactical approach to weak omega-groupoids. Zbl 1252.68058
Altenkirch, Thorsten; Rypacek, Ondrej
3
2012
From reversible to irreversible computations. Zbl 1279.68077
Green, Alexander S.; Altenkirch, Thorsten
3
2008
Normalization by evaluation for \(\lambda ^{\rightarrow 2}\). Zbl 1122.68393
Altenkirch, Thorsten; Uustalu, Tarmo
3
2004
A universe of strictly positive families. Zbl 1170.68432
Morris, Peter; Altenkirch, Thorsten; Ghani, Neil
3
2009
Higher-order containers. Zbl 1286.68327
Altenkirch, Thorsten; Levy, Paul; Staton, Sam
2
2010
A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029
Abel, Andreas; Altenkirch, Thorsten
2
2000
When is a function a fold or an unfold? Zbl 1260.68096
Gibbons, Jeremy; Hutton, Graham; Altenkirch, Thorsten
2
2001
The integers as a higher inductive type. Zbl 1498.03028
Altenkirch, Thorsten; Scoccola, Luis
2
2020
Setoid type theory – a syntactic translation. Zbl 1434.03034
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Tabareau, Nicolas
2
2019
Relative monads formalised. Zbl 1451.68330
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
2
2014
Exploring the regular tree types. Zbl 1172.68401
Morris, Peter; Altenkirch, Thorsten; McBride, Conor
1
2006
A partial type checking algorithm for Type:Type. Zbl 1291.68106
Abel, Andreas; Altenkirch, Thorsten
1
2011
Towards a cubical type theory without an interval. Zbl 1434.03035
Altenkirch, Thorsten; Kaposi, Ambrus
1
2018
Logical relations and inductive/coinductive types. Zbl 0934.03019
Altenkirch, Thorsten
1
1999
Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27–31, 1999. Selected papers. Zbl 0929.00065
1
1999
Constructing a universe for the setoid model. Zbl 07410416
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Sattler, Christian; Sestini, Filippo
1
2021
Constructing a universe for the setoid model. Zbl 07410416
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Sattler, Christian; Sestini, Filippo
1
2021
The integers as a higher inductive type. Zbl 1498.03028
Altenkirch, Thorsten; Scoccola, Luis
2
2020
Setoid type theory – a syntactic translation. Zbl 1434.03034
Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Tabareau, Nicolas
2
2019
Quotient inductive-inductive types. Zbl 1506.03063
Altenkirch, Thorsten; Capriotti, Paolo; Dijkstra, Gabe; Kraus, Nicolai; Nordvall Forsberg, Fredrik
11
2018
Free higher groups in homotopy type theory. Zbl 1453.03003
Kraus, Nicolai; Altenkirch, Thorsten
4
2018
Towards a cubical type theory without an interval. Zbl 1434.03035
Altenkirch, Thorsten; Kaposi, Ambrus
1
2018
Partiality, revisited. The partiality monad as a quotient inductive-inductive type. Zbl 1486.68036
Altenkirch, Thorsten; Danielsson, Nils Anders; Kraus, Nicolai
12
2017
Normalisation by evaluation for type theory, in type theory. Zbl 1459.03013
Altenkirch, Thorsten; Kaposi, Ambrus
7
2017
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
5
2017
Type theory in type theory using quotient inductive types. Zbl 1347.68045
Altenkirch, Thorsten; Kaposi, Ambrus
26
2016
Extending homotopy type theory with strict equality. Zbl 1370.03014
Altenkirch, Thorsten; Capriotti, Paolo; Kraus, Nicolai
7
2016
Normalisation by evaluation for dependent types. Zbl 1387.68060
Altenkirch, Thorsten; Kaposi, Ambrus
5
2016
Indexed containers. Zbl 1420.68032
Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; Mcbride, Conor; Morris, Peter
22
2015
Monads need not be endofunctors. Zbl 1448.18007
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
21
2015
Relative monads formalised. Zbl 1451.68330
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
2
2014
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
Small induction recursion. Zbl 1381.68189
Hancock, Peter; McBride, Conor; Ghani, Neil; Malatesta, Lorenzo; Altenkirch, Thorsten
9
2013
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
4
2013
A syntactical approach to weak omega-groupoids. Zbl 1252.68058
Altenkirch, Thorsten; Rypacek, Ondrej
3
2012
A categorical semantics for inductive-inductive definitions. Zbl 1344.68143
Altenkirch, Thorsten; Morris, Peter; Nordvall Forsberg, Fredrik; Setzer, Anton
5
2011
A partial type checking algorithm for Type:Type. Zbl 1291.68106
Abel, Andreas; Altenkirch, Thorsten
1
2011
Monads need not be endofunctors. Zbl 1284.18010
Altenkirch, Thorsten; Chapman, James; Uustalu, Tarmo
16
2010
Subtyping, declaratively. An exercise in mixed induction and coinduction. Zbl 1286.68074
Danielsson, Nils Anders; Altenkirch, Thorsten
10
2010
\(\Pi \Sigma \): dependent types without the sugar. Zbl 1284.68122
Altenkirch, Thorsten; Danielsson, Nils Anders; Löh, Andres; Oury, Nicolas
4
2010
The quantum IO monad. Zbl 1209.68103
Altenkirch, Thorsten; Green, Alexander S.
4
2010
Higher-order containers. Zbl 1286.68327
Altenkirch, Thorsten; Levy, Paul; Staton, Sam
2
2010
Big-step normalisation. Zbl 1191.68153
Altenkirch, Thorsten; Chapman, James
9
2009
A universe of strictly positive families. Zbl 1170.68432
Morris, Peter; Altenkirch, Thorsten; Ghani, Neil
3
2009
From reversible to irreversible computations. Zbl 1279.68077
Green, Alexander S.; Altenkirch, Thorsten
3
2008
An algebra of pure quantum programming. Zbl 1277.68053
Altenkirch, Thorsten; Grattage, Jonathan; Vizzotto, Juliana K.; Sabry, Amr
9
2007
Structuring quantum effects: superoperators as arrows. Zbl 1122.68062
Vizzotto, Juliana; Altenkirch, Thorsten; Sabry, Amr
9
2006
Exploring the regular tree types. Zbl 1172.68401
Morris, Peter; Altenkirch, Thorsten; McBride, Conor
1
2006
Containers: Constructing strictly positive types. Zbl 1077.68015
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
38
2005
\(\partial\) for data: Differentiating data structures. Zbl 1102.68020
Abbott, Michael; Altenkirch, Thorsten; McBride, Conor; Ghani, Neil
7
2005
Representing nested inductive types using W-types. Zbl 1099.03058
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
7
2004
Constructing polymorphic programs with quotient types. Zbl 1106.68335
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil; McBride, Conor
4
2004
Normalization by evaluation for \(\lambda ^{\rightarrow 2}\). Zbl 1122.68393
Altenkirch, Thorsten; Uustalu, Tarmo
3
2004
Categories of containers. Zbl 1029.68096
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil
29
2003
Generic programming within dependently typed programming. Zbl 1089.68529
Altenkirch, Thorsten; McBride, Conor
10
2003
Derivatives of containers. Zbl 1039.68078
Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil; McBride, Conor
9
2003
A predicative analysis of structural recursion. Zbl 0998.68027
Abel, Andreas; Altenkirch, Thorsten
11
2002
A finitary subsystem of the polymorphic \(\lambda\)-calculus. Zbl 0981.03020
Altenkirch, Thorsten; Coquand, Thierry
5
2001
Representations of first order function types as terminal coalgebras. Zbl 0981.68110
Altenkirch, Thorsten
4
2001
When is a function a fold or an unfold? Zbl 1260.68096
Gibbons, Jeremy; Hutton, Graham; Altenkirch, Thorsten
2
2001
A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. Zbl 0988.03029
Abel, Andreas; Altenkirch, Thorsten
2
2000
Monadic presentations of lambda terms using generalized inductive types. Zbl 0944.03011
Altenkirch, Thorsten; Reus, Bernhard
31
1999
Logical relations and inductive/coinductive types. Zbl 0934.03019
Altenkirch, Thorsten
1
1999
Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27–31, 1999. Selected papers. Zbl 0929.00065
1
1999
Categorical reconstruction of a reduction free normalization proof. Zbl 1502.03019
Altenkirch, Thorsten; Hofmann, Martin; Streicher, Thomas
8
1995
A formalization of the strong normalization proof for system F in LEGO. Zbl 0797.68095
Altenkirch, Thorsten
16
1993
all top 5

Cited by 315 Authors

14 Uustalu, Tarmo
11 Altenkirch, Thorsten
10 Veltri, Niccolò
9 Abel, Andreas M.
9 Ghani, Neil
7 Ahrens, Benedikt
7 McBride, Conor Thomas
6 Fiore, Marcelo P.
6 Maggesi, Marco
6 Matthes, Ralph
5 Hirschowitz, André
5 Kaposi, Ambrus
5 Kraus, Nicolai
5 Pientka, Brigitte
5 Vizzotto, Juliana Kaizer
4 Ahman, Danel
4 Angiuli, Carlo
4 Arrighi, Pablo
4 Coquand, Thierry
4 Lafont, Ambroise
4 Licata, Daniel R.
4 Sabry, Amr
4 Setzer, Anton
4 Staton, Sam
4 van der Weide, Niels
3 Allais, Guillaume
3 Birkedal, Lars
3 Boulier, Simon
3 Capretta, Venanzio
3 Chapman, James T. E.
3 Du Bois, André Rauber
3 Dybjer, Peter
3 Grattage, Jonathan
3 Gratzer, Daniel
3 Hancock, Peter G.
3 Harper, Robert
3 Hinze, Ralf
3 Hötzel Escardó, Martín
3 Jaskelioff, Mauro
3 Johann, Patricia
3 Nordvall Forsberg, Fredrik
3 Shulman, Michael A.
3 Stump, Aaron
3 Swierstra, Wouter
3 Zeilberger, Noam
2 Asai, Kenichi
2 Atkey, Robert
2 Ayala-Rincón, Mauricio
2 Benton, Nick
2 Berger, Ulrich
2 de Jong, Tom J.
2 Díaz-Caro, Alejandro
2 Dowek, Gilles
2 Feitosa, Samuel S.
2 Gambino, Nicola
2 Garner, Richard
2 Hasuo, Ichiro
2 Heunen, Chris
2 Hu, Jason Z. S.
2 Hutton, Graham
2 Hyland, J. Martin E.
2 Hyvernat, Pierre
2 Ishio, Chiaki
2 Jacobs, Bart
2 Jenkins, Christopher
2 Kennedy, Andrew J.
2 Kock, Joachim
2 Kovács, András
2 Lochbihler, Andreas
2 Lumsdaine, Peter LeFanu
2 Morris, Peter A.
2 Mörtberg, Anders
2 New, Max S.
2 Orchard, Dominic A.
2 Pfenning, Frank
2 Piróg, Maciej
2 Pitts, Andrew M.
2 Rennela, Mathys
2 Rivas, Exequiel
2 Sattler, Christian
2 Saville, Philip
2 Schäfer, Steven
2 Sestini, Filippo
2 Shan, Chung-chieh
2 Spitters, Bas
2 Steila, Silvia
2 Sterling, Jonathan
2 Stirton, William R.
2 Swan, Andrew W.
2 Tabareau, Nicolas
2 Traytel, Dmitry
2 Valiron, Benoît
2 Van den Berg, Benno
2 Voevodskiĭ, Vladimir Aleksandrovich
2 Voigtlander, Janis
1 Adelsberger, Stephan
1 Aehlig, Klaus
1 Al-Sibahi, Ahmad Salim
1 Alexander, Scott
1 Alpuim, Joao
...and 215 more Authors

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.