Teaching

I teach a series of courses on programming languages, logic, and type systems. For up-to-date, information on the courses please check the course schedule. All information with regard to courses is on mycourses.

Courses

COMP 302: Programming Languages and Paradigms

This course is designed to provide a thorough introduction to the foundations and paradigms of programming languages. In particular, we will investigate functional programming in theory and practice and learn about some of the considerations underlying functional and object-oriented programming. Some of the topics to be covered are functional programming in SML, lambda-calculus, type systems, continuations, the object-oriented paradigm, and subtyping.

COMP 523: Language-based security

Language-based security relies on techniques from programming languages such as automated program analysis, type checking, certifying compilers to enforce security policies in networked computing environments. This course looks at advanced principles of programming languages and verification techniques. In particular, we discuss mathematical foundations such as type systems, lambda calculus and proof theory, underlying the theory and practice of functional programming, as well as representation and verification of safety and security policies. We will particular attention to the formalization of the meta-theory about programing languages.

COMP 527: Logic and Computation

Logic provides computer science with both a unifying foundational framework and a tool for modeling. In fact, logic has been called "the calculus of computer science", playing a crucial role in diverse areas such as artificial intelligence, computational complexity, distributed computing, database systems, hardware design, programming languages, and software engineering This course is designed to provide a thorough introduction to modern constructive logic, its numerous applications in computer science, and its mathematical properties. Some of the topics to be covered are intuitionistic logic, functional and logic programming, type theory, theorem proving, unification, first-order logic, non-classical logics.

COMP 599: Certified Proofs and Programs (Special Topics)

>Dependent types allow us to track rich properties about the (partial) correctness of a program as part of the type. Such properties can then be verified statically via type checking prior to running the program. The power of this idea is far reaching: we can statically verify termination of many programs, check for array-bounce or track access control policies. In addition to checking rich properties statically, dependent types also allow us to certify that a program satisfies a given property allowing the programmer to construct and return an explicit proof object which can be validated independently. The course begins with a theoretical introduction to dependent types. We then survey the landscape of dependently typed programming and proof environments, its use in logical frameworks to represent proofs and explore its applications in proof-carrying code and mechanizing the meta-theory of formal systems.

COMP 762: Computation and Deduction

This course, we explore the theory and practice of logical frameworks. Logical frameworks offer a general meta-language to specify, implement, and execute formal systems given via axioms and inference rules. Furthermore, logical frameworks provide a common basis for the study of meta-theoretic properties (e.g., preservation of types under evaluation). Some of the topics to covered include: lambda-calculus, dependent types, higher-order abstract syntax, functional programming with higher-order data, reasoning with induction over higher-order data.

Related Courses

McGill offers a number of courses in logic and foundations of programming languages you may also find interesting.

Brigitte Pientka

Sidebar Menu