The following of my publications are less recent.
 A Compiled Implementation of Normalization by Evaluation
with Florian Haftmann and
Tobias Nipkow.
TPHOLs 2008.
Springer
LNCS
5170 (2008), 3954.
(Bib, slides);
Isabelle theories at the
Archive of Formal Proofs
(Bib).
A journal version appeared at the Journal of Functional Programming (Vol 22(1), 930).
 On the computational complexity of cutreduction
with Arnold
Beckmann.
LICS
2008.
(Bib)
Full technical details available as
Swansea University
Computer Science
technical report
CSR152007;
arXiv:0712.1499
(slides)
A journal version
appeared
Annals of Pure and
Applied Logic 161(6), 2010.
(Bib)
A somewhat related lecture on proof notations
was given at the Fall School in Logic 2008.
 Relativizing Small Complexity Classes
and their Theories
with
Stepen A. Cook and
Phuong The
Nguyen.
CSL 2007
LNCS 4646 (2007).
(Bib,
slides;
longer version
(ps))
An extended Version
(arXive/1204.5508)
is published in Computational Complexity 25(1), 2016
(Bib).
 Propositional Logic for Circuit
Classes
with Arnold Beckmann.
CSL 2007
LNCS 4646 (2007).
(Bib,
slides)
 Normalization by Evaluation for
MartinLöf Type Theory with one Universe, with
Andreas Abel and
Peter Dybjer.
Mathematical Foundations of Programming Semantics 2007.
(Bib)
 ParameterFree Polymorphic Types.
Annals of Pure and
Applied Logic, 156 (2008), 312.
(Bib)
 A Finite Semantics of SimplyTyped Lambda Terms
for Infinite Runs of Automata,
CSL 2006 LNCS 4207 (2006), 104118.
(pdf,
Bib,
slides).
A full version is
available at
Logical Methods in Computer Science.
(Bib)
arXiv:0706.2076
 The Monadic Second Order Theory of Trees
Given by Arbitrary LevelTwo Recursion Schemes Is Decidable
with
Jolie
G. de Miranda and
C.H. Luke
Ong.
(TLCA
2005).
Springer
LNCS
3461 (2005) 3954.
Bib.
slides
(old,
older).
 Safety is Not a Restriction at Level 2
for String Languages with
Jolie
G. de Miranda and
C.H. Luke
Ong.
(FOSSACS
2005).
Springer
LNCS
3441 (2005), 490504.
Bib.
(technical
report, Bib)
 Induction and Inductive Definitions in
Fragments of Second Order Arithmetic. Journal of Symbolic
Logic, 70(4) 2005, 10871107. Bib.

On Fragments of Analysis with Strengths of
Finitely Iterated Inductive Definitions. PhD thesis, supervised by
Wilfried
Buchholz;
defended on July 18, 2003.
Bib.
The defence talk (in German).
There are also
slides of a related talk in
Venice,
and
those of a similar
talk
in Swansea.
 Continous Normalization for the
LambdaCalculus and Gödel's T, with
Felix
Joachimski. (Annals of Pure and Applied Logic, 133(13)
(2005), 3971.)
pdf,
Bib.
 An
Elementary Fragment of SecondOrder Lambda Calculus,
with Jan Johannsen.
ACM Transactions on Computational Logic
6 (2005).
(Also presented at ICC
'02),
Bib,
arXiv.
 Operational Aspects of Untyped
Normalization by Evaluation, with
Felix
Joachimski.
Mathematical Structures in Computer Science (2004) 14:587611.
slides,
other slides,
Bib.
[Replaces an
obsolete draft of January 2001.
Bib,
scm.]
 On Continuous Normalization, with
Felix
Joachimski.
(CSL '02.
Springer
LNCS
2471),
Abstract,
Slides,
Bib.
 Linear Ramified Higher Type Recursion and Parallel Computation,
with
Jan
Johannsen,
Helmut
Schwichtenberg,
Sebastiaan
Terwijn
(Proof Theory in Computer Science.
Springer
LNCS
2183, pp. 121)
Bib,
Links
 Programmextraktion für nichtwachsende
Polynomialzeitberechnungen
(Diplomarbeit, Betreuer
Prof.
H. Schwichtenberg).
Slides,
Bib,
Links
 An arithmetic for
nonsizeincreasing...
 A
syntactical analysis of nonsizeincreasing polynomial time
computation, with
Helmut
Schwichtenberg
(LICS
2000).
Slides,
Bib,
Links
(a journal
version
is published in ACM
TOCL.
BiB,
arXiv)
 K. Aehlig.
The Parallelisation of a Finite Element Code on a
SharedMemory Computer using OpenMP.
(Final report of my project at a
Summer Scholarship Programme at the
Edinburgh Parallel Computing Center).
 R. Winkler, K. Aehlig.
Temporal
variation of thoron decay product concentration in the atmosphere and
comparison with radon decay product concentration.
Radiation
and Environmental Biophysics (1998)
37:
3539
 F. Ruckerbauer, K. Aehlig, R. Winkler. Zeitaufgelöste Messung
niedriger Radongaskonzentrationen.
gsfBericht 4/98
(Institut für Strahlenschutz, AG Radioökologie)
$Date: 2016/02/14 12:18:51 $