2019 - 2020

0368-3241   Programming Languages                                                                                
FACULTY OF EXACT SCIENCES
View groups
 
Course description

This course introduces basic concepts and techniques in the foundational study of programming languages, stressing their formal logical underpinnings. The central theme is the view of individual programs and programming languages as mathematical objects about which precise claims may be made and proven. The whole course will be taught using the Coq proof assistant, a popular interactive theorem prover implementing a dependently typed functional programming language. Particular topics include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism, and Hoare logic. 

Prior knowledge of Coq or functional programming is not required. Since Coq has a steep learning curve, the course will require considerable time and effort, including weekly homework and self-learning of some material that will not be covered in lectures and tutorials.

The main texts for the course are the online books available at [https://softwarefoundations.cis.upenn.edu].

accessibility declaration


tel aviv university