糖心原创

School of Computer Science
 

Image of Thorsten Altenkirch

Thorsten Altenkirch

Professor of Computer Science, Faculty of Science

Contact

Research Summary

Thorsten Altenkirch's main research interest is the application of constructive logic in Computer Science. Constructive logic diverges from classical logic in the rejection of the principle of the… read more

Selected Publications

  • ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2005. Theoretical Computer Science. 342(1), 3-27
  • ABBOTT, M., ALTENKIRCH, T., MCBRIDE, C. and GHANI, N., 2005. Fundamentae Informatica. 65(1/2), 1-28
  • ALTENKIRCH, T. and GRATTAGE, J., 2005. In: 20th Annual IEEE Symposium on Logic in Computer Science, Chicago, USA, 26-29 June 2005. 249-259
  • ALTENKIRCH, T., DYBJER, P., HOFMANN, M. and SCOTT, P., 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts In: 16th Annual IEEE Symposium on Logic in Computer Science.

Current Research

Thorsten Altenkirch's main research interest is the application of constructive logic in Computer Science. Constructive logic diverges from classical logic in the rejection of the principle of the excluded middle. As a consequence of this, a constructive proof of the existence of a certain object (e.g. a number) can be turned into a computer program to calculate this object.An example of a constructive logic is Type Theory, introduced by the Swedish philosopher Per Martin-L枚f. Type Theory is at the same time a programming language and a logic: propositions correspond to types and proofs to programs. Current research centers on theoretical aspects of Type Theory but also on the construction of elegant and efficient implementations of type theoretic languages. An example of this is the Epigram system, currently under development in Nottingham, which we use to develop programs which are correct by construction.Dr. Altenkirch's research covers applications of Category Theory as a formalism to concisely express abstract properties of mathematical constructions in Computer Science and the investigation of typed lambda calculi as a foundation of (functional) programming languages and Type Theory. He is interested in the computational nature of the physical universe and the practical exploitation of this nature, which is reflected in a research project on Quantum Computation. He is also fascinated by the development of the philosophical foundations of logic in a time when computing science replaces natural science as the prime application of abstract reasoning.For further information about his research, please consult .

  • THORSTEN ALTENKIRCH, NILS ANDERS DANIELSSON and NICOLAI KRAUS, 2017. In: Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 534-549
  • THORSTEN ALTENKIRCH and AMBRUS KAPOSI, 2017. Logical Methods in Computer Science. 13(4),
  • THORSTEN ALTENKIRCH, PAOLO CAPRIOTTI, GABE DIJKSTRA, NICOLAI KRAUS and FREDRIK NORDVALL FORSBERG, 2017.
  • ALTENKIRCH, THORSTEN and KAPOSI, AMBRUS, 2016. ACM SIGPLAN Notices. 51(1), 18-29
  • THORSTEN ALTENKIRCH and AMBRUS KAPOSI, 2016. In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. 6:1-6:16
  • THORSTEN ALTENKIRCH, PAOLO CAPRIOTTI and NICOLAI KRAUS, 2016. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. 21:1-21:17
  • THORSTEN ALTENKIRCH, JAMES CHAPMAN and TARMO UUSTALU, 2015. Logical Methods in Computer Science. 11(1:3), 1-40
  • ALTENKIRCH, THORSTEN, LI, NUO and RYP'AVCEK, ONDVREJ, 2014. In: Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. 4:1-4:8
  • THORSTEN ALTENKIRCH, JAMES CHAPMAN and TARMO UUSTALU, 2014. J. Formalized Reasoning. 7(1), 1-43
  • NICOLAI KRAUS, MART'IN H脰TZEL ESCARD脫, THIERRY COQUAND and THORSTEN ALTENKIRCH, 2013. Generalizations of Hedberg's Theorem In: Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. 173-188
  • PETER HANCOCK, CONOR MCBRIDE, NEIL GHANI, LORENZO MALATESTA and THORSTEN ALTENKIRCH, 2013. Small Induction Recursion In: Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013. 156-172
  • THORSTEN ALTENKIRCH and ONDREJ RYPACEK, 2012. A Syntactical Approach to Weak omega-Groupoids In: Computer Science Logic (CSL'12). 16-30
  • THORSTEN ALTENKIRCH, FREDRIK NORDVALL FORSBERG, PETER MORRIS and ANTON SETZER, 2011. A categorical semantics for inductive-inductive definitions. In: Fourth International Conference on Algebra and Coalgebra in Computer Science: CALCO 2011
  • ALTENKIRCH, T. and GREEN, A., 2010. . In: GAY, S. and MACKIE, I., eds., Semantic techniques in quantum computation Cambridge University Press. 173-205
  • ALTENKIRCH, T., CHAPMAN, J. and UUSTALU, T., 2010. . In: ONG, L., ed., Foundations of software science and computational structures: 13th international conference, FOSSACS 2010, held as part of the joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings Springer. 297-311
  • THORSTEN ALTENKIRCH, NILS ANDERS DANIELSSON, ANDRES L脰H and NICOLAS OURY, 2010. . In: Functional and Logic Programming Springer. 40-55
  • THORSTEN ALTENKIRCH, PAUL LEVY and SAM STATON, 2010. . In: Computability in Europe: CiE 2010
  • ALTENKIRCH, T. and CHAPMAN, J., 2009. Journal of Functional Programming. 19(3-4), 311-333
  • ALTENKIRCH, T. and MORRIS, P., 2009. In: 24th Annual IEEE Symposium on Logic in Computer Science. 277-285
  • MORRIS, P., ALTENKIRCH, T. and GHANI, N., 2007. Constructing Strictly Positive Families In: The Australasian Theory Symposium. 111-122
  • ALTENKIRCH, T., GRATTAGE, J., VIZZOTTO, J.K. and SABRY A., 2007. Electronic Notes in Theoretical Compter Science: 3rd International Workshop on Quantum Programming Languages. 170C, 23-47 (In Press.)
  • VIZZOTTO, J., ALTENKIRCH, T. and SABRY, A., 2006. Mathematical Structures in Computer Science. 16(3), 453-468
  • MORRIS, P., ALTENKIRCH, T. and MCBRIDE, C., 2006. In: Types for Proofs and Programs.
  • ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2005. Theoretical Computer Science. 342(1), 3-27
  • ABBOTT, M., ALTENKIRCH, T., MCBRIDE, C. and GHANI, N., 2005. Fundamentae Informatica. 65(1/2), 1-28
  • ALTENKIRCH, T. and GRATTAGE, J., 2005. In: 20th Annual IEEE Symposium on Logic in Computer Science, Chicago, USA, 26-29 June 2005. 249-259
  • ABBOTT, M., ALTENKIRCH, T. and GHANI, N., 2004. Representing Nested Inductive Types using W-types In: Automata, Languages and Programming. 59 - 71
  • ALTENKIRCH, T. and UUSTALU, T., 2004. In: Functional and Logic Programming. 260 - 275
  • ABBOTT, M., ALTENKIRCH, T., GHANI, N. and MCBRIDE, C., 2004. In: 7th International Conference on Mathematics of Program Construction.
  • ABOTT, M., ALTENKIRCH, T. and GHANI, N., 2003. . In: GORDON, A.D., ed., Foundations of software science and computational structures: 6th International Conference, FOSSACS 2003, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003: proceedings Berlin: Springer. 23-38
  • ABOTT, M., ALTENKIRCH, T., GHANI, N. and MCBRIDE, C., 2003. In: Typed Lambda Calculi and Applications, TLCA 2003.
  • ABEL, A. and ALTENKIRCH, T., 2002. Journal of Functional Programming. 12(1), 1-41
  • ALTENKIRCH, T. and MCBRIDE, C., 2002. In: Proceedings IFIP Working Conference on Generic Programming.
  • GIBBONS, J., HUTTON, G.M. and ALTENKIRCH, T., 2001. In: Proceedings of the 4th International Workshop on Coalgebraic Methods in Computer Science.
  • ALTENKIRCH, T., DYBJER, P., HOFMANN, M. and SCOTT, P., 2001. Normalization by Evaluation for Typed Lambda Calculus with Coproducts In: 16th Annual IEEE Symposium on Logic in Computer Science.
  • ALTENKIRCH, T. and COQUAND, T., 2001. In: Typed Lambda Calculi and Applications. 22-28
  • THORSTEN ALTENKIRCH and AMBRUS KAPOSI, Towards a cubical type theory without an interval Leibniz International Proceedings in Informatics.

School of Computer Science

糖心原创
Jubilee Campus
Wollaton Road
Nottingham, NG8 1BB

For all enquires please visit: