Thorsten Altenkirch

According to our database1, Thorsten Altenkirch authored at least 70 papers between 1993 and 2020.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
The Integers as a Higher Inductive Type.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019
Constructing quotient inductive-inductive types.
Proc. ACM Program. Lang., 2019

Preface.
Fundam. Informaticae, 2019

Big Step Normalisation for Type Theory.
Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

Setoid Type Theory - A Syntactic Translation.
Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018
Free Higher Groups in Homotopy Type Theory.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Pure Functional Epidemics: An Agent-Based Approach.
Proceedings of the 30th Symposium on Implementation and Application of Functional Languages, 2018

Quotient Inductive-Inductive Types.
Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017
Normalisation by Evaluation for Type Theory, in Type Theory.
Log. Methods Comput. Sci., 2017

Notions of Anonymous Existence in Martin-Löf Type Theory.
Log. Methods Comput. Sci., 2017

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016
Selected papers from Dependently Typed Programming 2010 - Overview.
Math. Struct. Comput. Sci., 2016

Quotient inductive-inductive types.
CoRR, 2016

Normalisation by Evaluation for Dependent Types.
Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Type theory in type theory using quotient inductive types.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Extending Homotopy Type Theory with Strict Equality.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015
Indexed containers.
J. Funct. Program., 2015

Monads need not be endofunctors.
Log. Methods Comput. Sci., 2015

Towards a Cubical Type Theory without an Interval.
Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

2014
Relative Monads Formalised.
J. Formaliz. Reason., 2014

Some constructions on ω-groupoids.
Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014

2013
Generalizations of Hedberg's Theorem.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Small Induction Recursion.
Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2012
A Syntactical Approach to Weak omega-Groupoids.
Proceedings of the Computer Science Logic (CSL'12), 2012

2011
A Partial Type Checking Algorithm for Type: Type.
Electron. Notes Theor. Comput. Sci., 2011

A Categorical Semantics for Inductive-Inductive Definitions.
Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010
Preface.
Fundam. Informaticae, 2010

Subtyping, Declaratively.
Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

Termination Checking in the Presence of Nested Inductive and Coinductive Types.
Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Hereditary Substitutions for Simple Types, Formalized.
Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

PiSigma: Dependent Types without the Sugar.
Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Higher-Order Containers.
Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

2009
Big-step normalisation.
J. Funct. Program., 2009

A Universe of Strictly Positive Families.
Int. J. Found. Comput. Sci., 2009

Indexed Containers.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

2008
From Reversible to Irreversible Computations.
Electron. Notes Theor. Comput. Sci., 2008

Dependent Types for Distributed Arrays.
Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008

2007
An Algebra of Pure Quantum Programming.
Electron. Notes Theor. Comput. Sci., 2007

Observational equality, now!
Proceedings of the ACM Workshop Programming Languages meets Program Verification, 2007

Beauty in the beast.
Proceedings of the ACM SIGPLAN Workshop on Haskell, 2007

Constructing Strictly Positive Families.
Proceedings of the Theory of Computing 2007. Proceedings of the Thirteenth Computing: The Australasian Theory Symposium (CATS2007). January 30, 2007

2006
Structuring quantum effects: superoperators as arrows.
Math. Struct. Comput. Sci., 2006

Generic Programming with Dependent Types.
Proceedings of the Datatype-Generic Programming - International Spring School, 2006

Tait in One Big Step.
Proceedings of the Workshop on Mathematically Structured Functional Programming, 2006

2005
Containers: Constructing strictly positive types.
Theor. Comput. Sci., 2005

for Data: Differentiating Data Structures.
Fundam. Informaticae, 2005

Epigram reloaded: a standalone typechecker for ETT.
Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

A Functional Quantum Programming Language.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

2004
Exploring the Regular Tree Types.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Constructing Polymorphic Programs with Quotient Types.
Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

Representing Nested Inductive Types Using W-Types.
Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Normalization by Evaluation for lambda<sup>-2</sup>.
Proceedings of the Functional and Logic Programming, 7th International Symposium, 2004

04381 Abstracts Collection - Dependently Typed Programming.
Proceedings of the Dependently Typed Programming, 12.09. - 17.09.2004, 2004

2003
Derivatives of Containers.
Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

Categories of Containers.
Proceedings of the Foundations of Software Science and Computational Structures, 2003

2002
A predicative analysis of structural recursion.
J. Funct. Program., 2002

Generic Programming within Dependently Typed Programming.
Proceedings of the Generic Programming, 2002

2001
When is a function a fold or an unfold?
Proceedings of the Coalgebraic Methods in Computer Science, 2001

A Finitary Subsystem of the Polymorphic lambda-Calculus.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Representations of First Order Function Types as Terminal Coalgebras.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

Normalization by Evaluation for Typed Lambda Calculus with Coproducts.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

1999
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
Proceedings of the Types for Proofs and Programs, 1999

Extensional Equality in Intensional Type Theory.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Monadic Presentations of Lambda Terms Using Generalized Inductive Types.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998
Logical Relations and Inductive/Coinductive Types.
Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1996
Reduction-Free Normalisation for a Polymorphic System.
Proceedings of the Fourth Israel Symposium on Theory of Computing and Systems, 1996

1995
Categorical Reconstruction of a Reduction Free Normalization Proof.
Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1993
Proving Strong Normalization of CC by Modifying Realizability Semantics.
Proceedings of the Types for Proofs and Programs, 1993

A Formalization of the Strong Normalization Proof for System F in LEGO.
Proceedings of the Typed Lambda Calculi and Applications, 1993

Constructions, inductive types and strong normalization.
PhD thesis, 1993


  Loading...