23FS MAT605 Logic and Foundations with Haskell
23FS MAT605 Logic and Foundations with Haskell
-
From Marius Furter
15 plays 0We 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
38 plays 0We 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
33 plays 0We cover the basic definitions of set theory in preparation for understanding the ZFC axioms. -
From Marius Furter
10 plays 0We 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
15 plays 0We 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
18 plays 0I 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
26 plays 0We discuss how the foldr and foldl patterns can be used for very compact implementations. -
From Marius Furter
33 plays 0We prove completeness of the natural deduction proof calculus for propositional logic. -
From Marius Furter
21 plays 0We implement natural numbers, arithmetic and comparison using an inductive datatype. All code can be found in the course git repository… -
From Marius Furter
66 plays 0We 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
45 plays 0We cover the semantic definitions for propositional logic which assign formulas truth values in a sigma-structure. -
From Marius Furter
26 plays 0We 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
58 plays 0We formally define the syntax of propositional logic and prove a unique parsing theorem for its formulas. -
From Marius Furter
17 plays 0We cover the basic definitions for relations and implement them in code. All code can be found in the course git repository… -
From Marius Furter
37 plays 0In this video we implement sets and associated functions. -
From Marius Furter
112 plays 0This video covers the formal proof system called natural deduction (without quantifiers), along with the corresponding sequent rules. -
From Marius Furter
42 plays 0In 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
76 plays 0This videos covers the rules for proving first order logic statements. A summary of the rules can be found at… -
From Marius Furter
60 plays 0I discuss how to define functions using pattern matching and guards. Then I introduce where, let and case expressions. -
From Marius Furter
76 plays 0We cover types, type variables, and typeclasses in Haskell. This video follows chapter 3 of "Learn you a Haskell for great good"…