BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Cyprus
1 × Czech Republic
1 × Finland
1 × France
1 × Italy
2 × Japan
2 × Poland
2 × Spain
2 × The Netherlands
4 × USA
Collaborated with:
∅ N.Ghani M.Abbott T.Uustalu Ambrus Kaposi T.Coquand N.Kraus M.Hofmann O.Rypacek P.Morris J.Grattage B.Reus W.Swierstra C.McBride J.Chapman T.Streicher P.Capriotti András Kovács M.H.Escardó N.A.Danielsson A.Löh N.Oury P.Dybjer P.J.Scott P.Hancock L.Malatesta
Talks about:
type (13) induct (7) theori (4) contain (3) normal (3) use (3) polymorph (2) quotient (2) function (2) calculus (2)

Person: Thorsten Altenkirch

DBLP DBLP: Altenkirch:Thorsten

Facilitated 1 volumes:

TLCA 2015Ed

Contributed to:

TLCA 20132013
CSL 20122012
FLOPS 20102010
FOSSACS 20102010
LICS 20092009
LICS 20052005
FLOPS 20042004
ICALP 20042004
FoSSaCS 20032003
TLCA 20032003
LICS 20012001
TLCA 20012001
CSL 19991999
LICS 19991999
CSL 19981998
LICS 19961996
TLCA 19931993
CSL 20162016
Haskell 20072007
POPL 20162016
POPL 20192019

Wrote 23 papers:

TLCA-2013-HancockMGMA #induction #recursion
Small Induction Recursion (PH, CM, NG, LM, TA), pp. 156–172.
TLCA-2013-KrausECA #theorem
Generalizations of Hedberg’s Theorem (NK, MHE, TC, TA), pp. 173–188.
CSL-2012-AltenkirchR #approach
A Syntactical Approach to Weak ω-Groupoids (TA, OR), pp. 16–30.
FLOPS-2010-AltenkirchDLO #dependent type #named
ΠΣ: Dependent Types without the Sugar (TA, NAD, AL, NO), pp. 40–55.
FoSSaCS-2010-AltenkirchCU #monad
Monads Need Not Be Endofunctors (TA, JC, TU), pp. 297–311.
LICS-2009-AltenkirchM
Indexed Containers (TA, PM), pp. 277–285.
LICS-2005-AltenkirchG #functional #programming language #quantum
A Functional Quantum Programming Language (TA, JG), pp. 249–258.
FLOPS-2004-AltenkirchU #evaluation #normalisation
Normalization by Evaluation for λ→2 (TA, TU), pp. 260–275.
ICALP-2004-AbbottAG #induction #representation #using
Representing Nested Inductive Types Using W-Types (MA, TA, NG), pp. 59–71.
FoSSaCS-2003-AbbottAG #category theory
Categories of Containers (MA, TA, NG), pp. 23–38.
TLCA-2003-AbbottAGM
Derivatives of Containers (MA, TA, NG, CM), pp. 16–30.
LICS-2001-AltenkirchDHS #evaluation #normalisation #λ-calculus
Normalization by Evaluation for Typed λ Calculus with Coproducts (TA, PD, MH, PJS), pp. 303–310.
TLCA-2001-Altenkirch #algebra #first-order
Representations of First Order Function Types as Terminal Coalgebras (TA), pp. 8–21.
TLCA-2001-AltenkirchC #polymorphism #λ-calculus
A Finitary Subsystem of the Polymorphic λ-Calculus (TA, TC), pp. 22–28.
CSL-1999-AltenkirchR #induction #monad #using
Monadic Presentations of λ Terms Using Generalized Inductive Types (TA, BR), pp. 453–468.
LICS-1999-Altenkirch #similarity #type system
Extensional Equality in Intensional Type Theory (TA), pp. 412–420.
CSL-1998-Altenkirch #induction #logic
Logical Relations and Inductive/Coinductive Types (TA), pp. 343–354.
LICS-1996-AltenkirchHS #normalisation #polymorphism
Reduction-Free Normalisation for a Polymorphic System (TA, MH, TS), pp. 98–106.
TLCA-1993-Altenkirch #formal method #normalisation #proving #system f
A Formalization of the Strong Normalization Proof for System F in LEGO (TA), pp. 13–28.
CSL-2016-AltenkirchCK #similarity #strict #type system
Extending Homotopy Type Theory with Strict Equality (TA, PC, NK), p. 17.
Haskell-2007-SwierstraA
Beauty in the beast (WS, TA), pp. 25–36.
POPL-2016-AltenkirchK #induction #type system #using
Type theory in type theory using quotient inductive types (TA, AK), pp. 18–29.
POPL-2019-KaposiKA #induction
Constructing quotient inductive-inductive types (AK, AK, TA), p. 24.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.