Have you been writing software for a while and now want to go deeper into the philosophy and mechanics of programming languages? Have you been hearing about things like automated theorem proving, hybrid type checking, gradual types, and wondering whether you'll be finding them soon in mainstream programming languages? Are you interested out-of-the-mainstream programming language paradigms like logic programming? Have you heard mathematical-sounding terms like lambda calculus and pi calculus, and wondering whether understanding them will make you a better programmer? If so, welcome.
We're focused less on spreading the gospel of functional programming (although we assume you know something about it) than on figuring out what makes programming languages of any paradigm expressive and reliable. And we try to take a more concrete approach than category theory's high-level overview of programming language structures, coming up with code we can execute and tools we can use.
This is the second of two talks in which Vlad Patryshev will show us implementation of category theory in Scala.
In the previous talk intuitionistic topologies of Grothendieck toposes were introduced. In this talk, Lawvere topologies are introduced.
Given an intuitionistic logic, a Lawvere topology defines levels of truthfulness approximation of statements in that logic. For example, a double negation logic maps a predicate into its double negation, making the resulting logic boolean.The accompanying code defines Lawvere topologies for a given topos, and can enumerate all possible topologies.
We'll post the link to the meeting on this page shortly before the scheduled start of the meeting.