Declarative Programming
A.Y. 2020/2021
Learning objectives
The aim of the course is to provide the students with a solid understanding of declarative programming, in the functional and logic flavor. The peculiarity of the course is to see the latter as an extension of the former. We will apply the paradigm to several areas, including automated theorem proving and the semantics of programming
languages.
languages.
Expected learning outcomes
Students will be able to write programs of medium complexity in both paradigms and appreciate their complementary features
Lesson period: Second semester
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
Second semester
Lectures: synchronous videolectures via Teams, based on slides and notes with a tablet. We shall propose exercises to be done by the student on the spot with the (free) software used in the course that the student will have to install.
Lectures will be recorded and made available for the duration of the semester
Midterm and final written exam to be taken in person (if possible).
Part B
Lectures will be recorded and made available for the duration of the semester
Midterm and final written exam to be taken in person (if possible).
Part B
Course syllabus
Part 1: the functional paradigm (F#)
1.1 Intro
- building blocks
- recursion and iteration
- typing and polymorphism
- algebraic data types
- property based testing
- higher-order functions
- lazy evaluation
- abstract data types
1.2 Case studies
1.2.1 Type checking and type inference
1.2.3 Logic: satisfability, tautology checking, normal forms.
--------------------------------------------
Part 2: the relational paradigm
(Twelf)
- facts, rules and queries
- unification and proof search
- examples
+ knowledge representation
+ combinatorial examples (8 queens)
- mode, coverage e termination checking
- PL examples, revisited:
+ interpreters and type checkers for MiniML
+ dependent types for type preserving computations
1.1 Intro
- building blocks
- recursion and iteration
- typing and polymorphism
- algebraic data types
- property based testing
- higher-order functions
- lazy evaluation
- abstract data types
1.2 Case studies
1.2.1 Type checking and type inference
1.2.3 Logic: satisfability, tautology checking, normal forms.
--------------------------------------------
Part 2: the relational paradigm
(Twelf)
- facts, rules and queries
- unification and proof search
- examples
+ knowledge representation
+ combinatorial examples (8 queens)
- mode, coverage e termination checking
- PL examples, revisited:
+ interpreters and type checkers for MiniML
+ dependent types for type preserving computations
Prerequisites for admission
None. We suggest you have taken Logic, programming and Algorithms
Teaching methods
(video)lectures and labs
Teaching Resources
Web page:
https://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
References:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: Lecure Notes by Frank Pfenning:
Logic programming https://www.cs.cmu.edu/~fp/courses/lp/
Computation and Deduction https://www.cs.cmu.edu/~fp/courses/comp-ded/
https://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
References:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: Lecure Notes by Frank Pfenning:
Logic programming https://www.cs.cmu.edu/~fp/courses/lp/
Computation and Deduction https://www.cs.cmu.edu/~fp/courses/comp-ded/
Assessment methods and Criteria
The exams takes place in the lab and consists of writing short programs on topics covered in the course. The grade on a 1-30 scale will depend on the correctness and elegance of the given solutions.
INF/01 - INFORMATICS - University credits: 6
Lessons: 48 hours
Professors:
Fiorentini Camillo, Momigliano Alberto Davide Adolfo
Professor(s)