The connection between formal logic, computational calculi, and mathematics in the area of category theory is a deep and profound one that is known as the Curry-Howard-Lambek correspondence. It is also known as the “propositions-as-types” (or “proofs-as-programs”)
paradigm and is at the core of the field of Type Theory. The theory of types was originally devised by Bertrand Russell to work around the set theoretic paradox of self-referentiality known as Russell’s paradox, it was propelled forward by the discovery
of the lambda calculus by Alonzo Church when the foundations for what modern computing and programming languages were laid by him, Turing, and Gödel responding in the negative to the “Entscheidungsproblem”. When Martin-Löf presented his landmark type
theory in the 70’s and 80’s he was building on the constructivist, or intuitionistic, principles from the school of Brouwer. This dependent type theory has served to usher in a new era of type theory with much progress. While the overarching goal of the
field is to establish type theory as a foundation for mathematics as a language in which mathematics is written, the major breakthroughs in in recent decades has been within computerized proof systems, which are, as far as I am aware, all based on Martin-Löfs
theory.
One such computerized proof system is Agda which is a dependently typed functional programming language, and therefore based on lambda calculus as well as Martin-Löf type theory. In this project I will lay the foundation, on which further work in the form of a master’s thesis can be done, by studying lambda calculus, formal semantics of programming languages, and become comfortable with Agda. The main aim of this is to become capable of reasoning and modeling programming languages in type theory, and to investigate the nature of the problems of including recursion and state, which is an innate issue since type theory is designed to assert termination of programs, - e.g Agda is total in this sense.
Metode:
Mathematical reasoning and coding in Agda. I will study relevant literature, specifically: ‘Programming Language Foundations in Agda’ by Wadler, Kokke, and Siek; ‘The Formal Semantics of Programming Languages: An Introduction’ by Winskel; ‘Introduction to Lambda Calculus’ by Barendregt and Barendsen.
Hvad afleveres:
As a deliverable I will implement a model of a functional programming language with in Agda, and write a report which I will hand in together with Agda code.
One such computerized proof system is Agda which is a dependently typed functional programming language, and therefore based on lambda calculus as well as Martin-Löf type theory. In this project I will lay the foundation, on which further work in the form of a master’s thesis can be done, by studying lambda calculus, formal semantics of programming languages, and become comfortable with Agda. The main aim of this is to become capable of reasoning and modeling programming languages in type theory, and to investigate the nature of the problems of including recursion and state, which is an innate issue since type theory is designed to assert termination of programs, - e.g Agda is total in this sense.
Metode:
Mathematical reasoning and coding in Agda. I will study relevant literature, specifically: ‘Programming Language Foundations in Agda’ by Wadler, Kokke, and Siek; ‘The Formal Semantics of Programming Languages: An Introduction’ by Winskel; ‘Introduction to Lambda Calculus’ by Barendregt and Barendsen.
Hvad afleveres:
As a deliverable I will implement a model of a functional programming language with in Agda, and write a report which I will hand in together with Agda code.
- Teacher: Rasmus Ejlers Møgelberg