First cycle
degree courses
Second cycle
degree courses
Single cycle
degree courses
School of Science
COMPUTER SCIENCE
Course unit
LOGICAL FOUNDATIONS OF FUNCTIONAL LANGUAGES
SC03119888, A.A. 2015/16

Information concerning the students who enrolled in A.Y. 2015/16

Information on the course unit
Degree course Second cycle degree in
COMPUTER SCIENCE
SC1176, Degree course structure A.Y. 2014/15, A.Y. 2015/16
N0
bring this page
with you
Number of ECTS credits allocated 6.0
Type of assessment Mark
Course unit English denomination LOGICAL FOUNDATIONS OF FUNCTIONAL LANGUAGES
Website of the academic structure http://informatica.scienze.unipd.it/2015/laurea_magistrale
Department of reference Department of Mathematics
Mandatory attendance No
Language of instruction Italian
Branch PADOVA
Single Course unit The Course unit can be attended under the option Single Course unit attendance
Optional Course unit The Course unit can be chosen as Optional Course unit

Lecturers
Teacher in charge SILVIO VALENTINI
Other lecturers MARIA EMILIA MAIETTI MAT/01

ECTS: details
Type Scientific-Disciplinary Sector Credits allocated
Educational activities in elective or integrative disciplines MAT/01 Mathematical Logic 6.0

Course unit organization
Period Second semester
Year 1st Year
Teaching method frontal

Type of hours Credits Teaching
hours
Hours of
Individual study
Shifts
Practice 1.0 8 17.0 No turn
Lecture 5.0 40 85.0 No turn

Calendar
Start of activities 01/03/2016
End of activities 15/06/2016
Show course schedule 2019/20 Reg.2014 course timetable

Examination board
Examination board not defined

Syllabus
Prerequisites: Some basic knowledge in mathematical logic and set theory
Target skills and knowledge: The aim of this course is to provide a basic theoretical introduction to typed and non-typed functional programming.
Examination methods: Homeworks and oral exam. The student is required to discuss his solutions of some homeworks.
Assessment criteria: The exam will assess the knowledge acquired by the student on the topics of the course and his ability to use it on practical example.
Course unit contents: We first present the pure lambda calculus and show that all recursive functions are lambda-representable. Then we move to the simply typed lambda calculus, we study its relation with the implicative fragment of the intuitionistic propositional calculus and prove that it is strongly normalising by interpreting types into saturated subsets of lambda terms. To gain further expressivity other types are then introduced which have a direct interpretation in intuitionistic logic or in constructive set theory arriving in the end to polymorphic typed lambda calculus. For all the considered calculi we prove the main theorems of strong normalization and confluence and in some cases we also study the categorical semantics and its application to the categorical abstract machine.
Planned learning activities and teaching methods: Classroom lessons
Additional notes about suggested reading: Lecture notes
Textbooks (and optional supplementary readings)
  • J.Y.Girard, Y.Lafont, P.Taylor, Proofs and Types. --: Cambridge University Press, --. Cerca nel catalogo
  • H.Barendreght, The Lambda Calculus, its Syntax and Semantics. --: North-Holland, --. Cerca nel catalogo
  • H.Barendreght,, Lambda Calculi with Types. --: Oxford University Press, --. Handbook of Logic in Computer Science Cerca nel catalogo