Thorsten Altenkirch

Thorsten Altenkirch's AcademicInfluence.com Rankings

Thorsten Altenkirch

Computer Science

#1304

World Rank

#1347

Historical Rank

Database

#8929

World Rank

#9387

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Thorsten Altenkirch's Degrees

PhD Computer Science University of Nottingham
Masters Computer Science University of Nottingham

Similar Degrees You Can Earn

Why Is Thorsten Altenkirch Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Thorsten Altenkirch is a German Professor of Computer Science at the University of Nottingham known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on univalent foundations at the Institute for Advanced Study. At Nottingham he co-chairs the Functional Programming Laboratory with Graham Hutton.

(See a Problem?)

Thorsten Altenkirch's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Containers: Constructing strictly positive types (2005) (204)
Monadic Presentations of Lambda Terms Using Generalized Inductive Types (1999) (179)
Categories of Containers (2003) (141)
Monads need not be endofunctors (2010) (133)
Observational equality, now! (2007) (133)
Indexed Containers (2009) (127)
Generic Programming within Dependently Typed Programming (2002) (99)
Categorical Reconstruction of a Reduction Free Normalization Proof (1995) (98)
Normalization by evaluation for typed lambda calculus with coproducts (2001) (94)
Type theory in type theory using quotient inductive types (2016) (88)
A Formalization of the Strong Normalization Proof for System F in LEGO (1993) (87)
Constructions, inductive types and strong normalization (1993) (82)
Extensional equality in intensional type theory (1999) (71)
Beauty in the beast (2007) (61)
A predicative analysis of structural recursion (2002) (58)
for Data: Differentiating Data Structures (2004) (53)
An Algebra of Pure Quantum Programming (2005) (47)
Extending Homotopy Type Theory with Strict Equality (2016) (46)
Structuring quantum effects: superoperators as arrows (2005) (45)
Generic Programming with Dependent Types (2006) (45)
Derivatives of Containers (2003) (44)
When is a function a fold or an unfold? (2001) (43)
Quotient inductive-inductive types (2016) (42)
A user's guide to {ALF (1994) (40)
The Quantum IO Monad (2006) (37)
Constructing quotient inductive-inductive types (2019) (36)
Exploring the Regular Tree Types (2004) (35)
Notions of Anonymous Existence in Martin-Löf Type Theory (2016) (35)
Constructing Polymorphic Programs with Quotient Types (2004) (33)
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2016) (32)
Reduction-free normalisation for a polymorphic system (1996) (31)
Beauty in the Beast A Functional Semantics for the Awkward Squad (2007) (31)
Subtyping, Declaratively (2010) (28)
Representations of First Order Function Types as Terminal Coalgebras (2001) (28)
A Categorical Semantics for Inductive-Inductive Definitions (2011) (27)
PiSigma: Dependent Types without the Sugar (2010) (26)
Towards Observational Type Theory (2006) (26)
Epigram reloaded: a standalone typechecker for ETT (2005) (25)
Representing Nested Inductive Types Using W-Types (2004) (24)
Homotopy Type Theory: Univalent Foundations of Mathematics (2013) (23)
Small Induction Recursion (2013) (22)
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types (1999) (22)
Normalisation by Evaluation for Dependent Types (2016) (21)
Proving Strong Normalization of CC by Modifying Realizability Semantics (1994) (20)
Normalisation by Evaluation for Type Theory, in Type Theory (2016) (20)
Constructing Strictly Positive Families (2007) (20)
Mixing Induction and Coinduction (2009) (20)
A Universe of Strictly Positive Families (2009) (20)
Generalizations of Hedberg's Theorem (2013) (19)
Hereditary substitutions for simple types, formalized (2010) (18)
Normalization by evaluation for λ→2 (2004) (18)
Big-step normalisation (2009) (18)
Subtyping, declaratively: an exercise in mixed induction and coinduction (2010) (18)
Logical Relations and Inductive/Coinductive Types (1998) (17)
Termination Checking in the Presence of Nested Inductive and Coinductive Types (2010) (17)
Normalization by Evaluation for lambda-2 (2004) (15)
From Reversible to Irreversible Computations (2008) (15)
QML : Quantum data and control (2005) (14)
Towards a Cubical Type Theory without an Interval (2015) (14)
A Syntactical Approach to Weak omega-Groupoids (2012) (12)
Relative Monads Formalised (2014) (12)
Setoid Type Theory - A Syntactic Translation (2019) (11)
Small Induction Recursion , Indexed Containers and Dependent Polynomials are equivalent ∗ (2012) (11)
A Syntactical Approach to Weak ω-Groupoids (2012) (11)
Tait in One Big Step (2006) (9)
A semantical analysis of structural recursion (2002) (9)
Dependent Types for Distributed Arrays (2008) (9)
Free Higher Groups in Homotopy Type Theory (2018) (9)
Pure Functional Epidemics: An Agent-Based Approach (2018) (8)
A Partial Type Checking Algorithm for Type: Type (2011) (8)
A Finitary Subsystem of the Polymorphic lambda-Calculus (2001) (8)
A Compiler for a Functional Quantum Programming Language (2005) (8)
The Integers as a Higher Inductive Type (2020) (7)
ΠΣ : A Core Language for Dependently Typed Programming (2008) (7)
Reduction-free Normalisation for System F Reduction-free Normalisation for System F (1996) (7)
A syntax for cubical type theory ( draft ) (2014) (6)
Some constructions on ω-groupoids (2014) (6)
Higher-Order Containers (2010) (5)
Types for proofs and programs : International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998 : selected papers (1999) (4)
What is the next programming paradigm (2012) (3)
Naïve Type Theory (2019) (3)
Higher Categories in Homotopy Type Theory (2016) (3)
Languages and Computation (G52LAC) Lecture notes Spring 2017 (2017) (2)
Towards Higher Observational Type Theory (2022) (2)
Normalization by hereditary substitutions (2010) (2)
A pr 2 00 5 A functional quantum programming language (2005) (2)
Proceedings of the 7th workshop on Programming languages meets program verification (2009) (2)
Constructing Strictly Positive Types (2004) (2)
Types for Proofs and Programs (2001) (1)
Chapter 1 Shor in Haskell The Quantum IO Monad (2008) (1)
A Functional Semantics for the Awkward Squad (2007) (1)
Constructing a universe for the setoid model (2021) (1)
Martin Hofmann’s contributions to type theory: Groupoids and univalence (2021) (1)
Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers (2007) (1)
Dependently Typed Programming 3 Computation by Judgement Rewriting (2005) (0)
Preface (2019) (0)
Draft Mixing Induction and Coinduction (2009) (0)
Should Type Theory Replace Set Theory as the Foundation of Mathematics? (2021) (0)
Generic Programming for Dependent Types Constructing Strictly Positive Families (2006) (0)
Big Step Normalisation for Type Theory (2019) (0)
University of Birmingham Quotient inductive-inductive types (2018) (0)
FUNCTIONAL PEARLS α-conversion is easy (2002) (0)
Machines and their languages (G51MAL) Lecture notes Spring 2003 (2004) (0)
18 A Syntactical Approach to Weak ω-Groupoids (2012) (0)
Decidability of equality for a simply typed calculus using hereditary substitutions in Agda (2010) (0)
Proceedings of the 2006 international conference on Types for proofs and programs (2006) (0)
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland (2015) (0)
2 ConstructingQuotient Inductive-Inductive Types (2018) (0)
Agda formalizations for article "Constructing Quotient Inductive-Inductive Types" (2018) (0)
Author index (1993) (0)
Λ-calculus and Types Lecture Notes Midland Graduate School / Appsem Spring School 2004 (2004) (0)
Programming + Veriication = Progiication (2007) (0)
26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy (2021) (0)
Preface (2010) (0)
Machines and their languages (G52MAL) Lecture notes Autumn 2007 (2007) (0)
Front Matter, Table of Contents, Preface, Conference Organization (2015) (0)
04381 Abstracts Collection - Dependently Typed Programming (2004) (0)
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009 (2009) (0)
Selected papers from Dependently Typed Programming 2010 – Overview (2014) (0)
Type Theory in Type Theory (draft) (2016) (0)
Programming + Verification = Progification ( Draft ) (0)
Integrated Veriication in Type Theory (lecture Notes) (1996) (0)
Pure functional epidemics (2018) (0)
Altenkirch, Thorsten and Kaposi, Ambrus (2016) Type theory in type theory using quotient inductive types. In: POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 20-22 January 2016, St Petersburg, Florida, United States of America (2017) (0)
Selected papers from the International Workshop on Types for Proofs and Programs (1998) (0)

This paper list is powered by the following services:

Other Resources About Thorsten Altenkirch

What Schools Are Affiliated With Thorsten Altenkirch?

Thorsten Altenkirch is affiliated with the following schools:

Thorsten Altenkirch's Academic­Influence.com Rankings