Essay CM50262 Functional Programming
Essay
Research question: Type theory (20 Marks)
Assignment Write a short essay (1000–1500 words) on the historical and contemporary
significance of type theory. Your essay should address the following points:
• the historical background of type theory
• the Curry-Howard correspondence (also called the Curry-Howard isomorphism or the
propositions-as-types correspondence)
• the influence of type theory on modern languages such as Agda and Coq, with an
example showing how their types are more powerful than those of Haskell
• examples to illustrate the importance of type theory in modern mathematics or com-
puter science
You should make use of the scientific literature on programming and mathematics to inform
your answer. You may find many Wikipedia entries and blog posts about type theory, Coq,
Agda and so on. These are a good starting point in your search for literature to refer to,
but are not definitive references. By all means use them to develop your understanding,
but you should aim to seek out scientific research papers, textbook descriptions, and similar
definitive documents to support your answer. Marks are allocated not only for your answer
but also for the choice of reference sources and the presentation of your bibliography.
Submission and Marking Scheme
Submit your essay as a PDF file named Essay.pdf on Moodle, for the assignment labelled
Essay, by the 30 April 8pm deadline. Preferably, write your essay using appropriate software
such as LATEX or Word. You may write it by hand and scan it to PDF. Please ensure the
document is clearly legible and well presented. The 20 marks available for this assignment
are allocated as follows:
• historical background: 4 marks
• Curry-Howard correspondence: 4 marks
• influence on modern functional languages: 4 marks
• examples illustrating importance: 4 marks
• literature sources and bibliography: 4 marks






























学霸联盟