Research themes in Logic and Computation

ABSTRACT

Logic has a very long history with many rebirths. Classically, it belongs to Philosophy; but, from mid XIX Century, when it received a new impulse from questions about the foundations of Mathematics, became itself a part of Mathematics. XX Century saw another rebirth: we may say Logic created Computer Science (even before there were any computers), but then Computer Science offered Logic a new youth. The relationship between Logic and Compu- tation is very rich: Logic is, of course, indispensable in the effort of mechanizing reasoning; Logic is a factory of formalisms and artificial languages; and Logic is a safe toolkit whenever Computer Science enters new domains (e.g. quantum computing). In this seminar we will give an overview of these relationships, and introduce some research themes in the area of Logic and Computation that can be pursued at DMA-UMinho. These themes belong, specifically, to the areas of proof theory and λ-calculus [2, 3, 1, 7, 5, 4, 6], which are of fundamental importance for the theory and design of programming languages and theorem provers.

References

  1. [1]  H. Barendregt. The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic, 3(2):181–215, 1997.
  2. [2]  H.P. Barendregt. The Lambda Calculus. North-Holland, 1984.
  3. [3]  J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press,

    1989.

  4. [4]  S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2008.
  5. [5]  M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
  6. [6]  Coq Team. Coq docs. Technical report, INRIA. http://coq.inria.fr/documentation.
  7. [7]  A. Troelstra and H. Schwitchtenberg. Basic Proof Theory. Cambridge University Press, second edition, 2000.