23FS MAT605 Logic and Foundations with Haskell
23FS MAT605 Logic and Foundations with Haskell
-
From Marius Furter
We look at three modules that include Rational and Complex numbers as well as Polynomials. We use these to implement Newton's method. All code can be found in the… -
From Marius Furter
We build the foundations of set theory using the Zermelo-Fraenkel axioms with choice. The material follows the first chapter of Thomas Jech's "Set Theory". -
From Marius Furter
We cover the basic definitions of set theory in preparation for understanding the ZFC axioms. -
From Marius Furter
We implements datatypes for integers based in the natural numbers. All code can be found in the course git repository https://github.com/MariusFurter/MAT605-haskell-FS23 -
From Marius Furter
We implement the typeclasses Ord, Enum, Num, Real and Integral for the natural numbers. This allows us to use all standard functions for these typeclasses on our natural… -
From Marius Furter
I show how the Maybe datatype and lists can be used to deal with functions that return either no value or multiple values. -
From Marius Furter
We discuss how the foldr and foldl patterns can be used for very compact implementations. -
From Marius Furter
We prove completeness of the natural deduction proof calculus for propositional logic. -
From Marius Furter
We implement natural numbers, arithmetic and comparison using an inductive datatype. All code can be found in the course git repository… -
From Marius Furter
We show that the natural deduction proof calculus is sound for propositional logic, meaning that it only proves true formulas given true assumptions. -
From Marius Furter
We cover the semantic definitions for propositional logic which assign formulas truth values in a sigma-structure. -
From Marius Furter
We implement functions as sets of pairs in Haskell. All code can be found in the course git repository https://github.com/MariusFurter/MAT605-haskell-FS23 -
From Marius Furter
We formally define the syntax of propositional logic and prove a unique parsing theorem for its formulas. -
From Marius Furter
We cover the basic definitions for relations and implement them in code. All code can be found in the course git repository… -
-
From Marius Furter
This video covers the formal proof system called natural deduction (without quantifiers), along with the corresponding sequent rules. -
From Marius Furter
In this video we implement our own version of the type Bool, along with the functions in the standard library that act on Bool. -
From Marius Furter
This videos covers the rules for proving first order logic statements. A summary of the rules can be found at… -
From Marius Furter
I discuss how to define functions using pattern matching and guards. Then I introduce where, let and case expressions. -
From Marius Furter
We cover types, type variables, and typeclasses in Haskell. This video follows chapter 3 of "Learn you a Haskell for great good"…