• A Compiled Implementation of Normalization by Evaluation with Florian Haftmann and Tobias Nipkow. TPHOLs 2008. Springer LNCS 5170 (2008), 39-54. (Bib, slides);
  Isabelle theories at the Archive of Formal Proofs (Bib). A journal version appeared at the Journal of Functional Programming (Vol 22(1), 9-30).
• On the computational complexity of cut-reduction with Arnold Beckmann. LICS 2008. (Bib)
  Full technical details available as Swansea University Computer Science technical report CSR15-2007; 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 Martin-Löf Type Theory with one Universe, with Andreas Abel and Peter Dybjer. Mathematical Foundations of Programming Semantics 2007. (Bib)
• Parameter-Free Polymorphic Types. Annals of Pure and Applied Logic, 156 (2008), 3-12. (Bib)
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata, CSL 2006 LNCS 4207 (2006), 104-118. (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 Level-Two Recursion Schemes Is Decidable with Jolie G. de Miranda and C.-H. Luke Ong. (TLCA 2005). Springer LNCS 3461 (2005) 39-54. 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), 490-504. Bib. (technical report, Bib)
• Induction and Inductive Definitions in Fragments of Second Order Arithmetic. Journal of Symbolic Logic, 70(4) 2005, 1087-1107. 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 Lambda-Calculus and Gödel's T, with Felix Joachimski. (Annals of Pure and Applied Logic, 133(1-3) (2005), 39-71.) pdf, Bib.
• An Elementary Fragment of Second-Order 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:587-611. 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. 1-21) Bib, Links
• Programmextraktion für nicht-wachsende Polynomialzeitberechnungen (Diplomarbeit, Betreuer Prof. H. Schwichtenberg). Slides, Bib, Links
• An arithmetic for non-size-increasing...
• A syntactical analysis of non-size-increasing 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 Shared-Memory 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: 35-39
• F. Ruckerbauer, K. Aehlig, R. Winkler. Zeitaufgelöste Messung niedriger Radongaskonzentrationen. gsf-Bericht 4/98 (Institut für Strahlenschutz, AG Radioökologie)
  

$Date: 2016/02/14 12:18:51 $