curry howard podcasts

Kodsnack 612 - Where types first come in, with Pedro Abreu

Play Episode Listen Later Nov 26, 2024 55:53

Fredrik talks to Pedro Abreu about the magical world of type theory. What is it, and why is it useful to know about and be inspired by? Pedro gives us some background on type theory, and then we talk about how type theory can provide new ways of reasoning about programs, and tools beyond tests to verify program correctness. This doesn’t mean that all languages should strive for the nirvana of dependent types, but knowing the tools are out there can come in handy even if the code you write is loosely typed. We wrap up with some further podcast tips, of course including Pedro’s own podcast Type theory forall. Thank you Cloudnet for sponsoring our VPS! Comments, questions or tips? We a re @kodsnack, @tobiashieta, @oferlund and @bjoreman on Twitter, have a page on Facebook and can be emailed at info@kodsnack.se if you want to write longer. We read everything we receive. If you enjoy Kodsnack we would love a review in iTunes! You can also support the podcast by buying us a coffee (or two!) through Ko-fi. Links Pedro Type theory Type theory forall - Pedro’s podcast Chalmers The meetup group through which Pedro and Fredrik met Purdue university Bertrand Russell The problem of self reference Types Set theory Kurt Gödel Halting problem Alan Turing Turing machine Alonzo Church Lambda calculus Rust Dependent types Formal methods Liquid types - Haskell extension SAT solver Property-based testing Quickcheck Curry-Howard isomorphism Support Kodsnack on Ko-fi! Functional programming Imperative programming Object-oriented programming Monads Monad transformers Lenses Interactive theorem provers Isabelle HOL Dafny Saul Crucible Symbolic execution CVC3, CVC5 solvers Pure functions C# Algebraic data types Pattern matching Scala Recursion Type theory forall episode 17: the first fantastic one with Conal Elliot. The discussion continues in episode 21 Denotational types Coq IRC Software foundations - about Coq and a lot more The church of logic podcast The Iowa type theory commute podcast Titles Type theory podcasts Very odd for some people Brazilian weather Relearning to appreciate The dawn of computer science Layers of sets Where types first come in Bundle values together The research about programming languages If you squint your eyes enough Nirvana of type systems Proofs all the way down Extra guarantees If your domain is infinite Formal guarantees The properties of my system What is the meaning of my program? Building better systems

technology building data virtual iowa software types proof pure brazilian property nirvana pattern ko functional rust titles purdue layers interactive liquid object purdue university formal bundle crucible dependent fredrik imperative hol lenses abreu turing scala symbolic alan turing chalmers proofs lambda vps irc haskell relearning bertrand russell halting quickcheck recursion coq monad kurt g chalmers university algebraic c sharp monads kodsnack curry howard alonzo church cloudnet

#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi

Type Theory Forall

Play Episode Listen Later Aug 29, 2024 112:49

In this episode we talk with Fabrizio Montesi, a Full Professor at the University of South Denmark. He is one of the creators of the Jolie Programming Language, President of the Microservices Community and Author of the book 'Introduction to Choreographies'. In today's episode we talk about the formal side of Distributed Sytems, session types, the calculi that model distributed systems, their type systems, their Curry-Howard correspondences, and all the main ideas around these concepts. Links Fabrizio's Website Fabrizio's Linkedin Fabrizio's X / Twitter Fabrizio's Mastodon Fabrizio's Youtube Jolie's Website

university president fabrizio microservices full professor distributed systems montesi curry howard

More on basics of simple types

Iowa Type Theory Commute

Play Episode Listen Later Apr 29, 2024 15:45

I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.

simple basics types curry howard

Normalization in type theory: where it is needed, and where not

Iowa Type Theory Commute

Play Episode Listen Later Mar 6, 2020 16:28

Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics) for conversion checking. This is the process of confirming that types are equivalent during type checking, which, due to dependent types, can require checking program equivalence. The latter is usually restricted to just beta-equivalence (where beta-reduction is substitution of argument for input variable when applying a function), because richer notions of program equivalence are usually undecidable. I have a mini-rant in this episode explaining why this usual requirement of normalization for conversion checking is not sensible.Also I note that you can find the episodes of the podcast organized by chapter on my web page.

conversion traditionally normalization type theory curry howard

Introduction to normalization

Iowa Type Theory Commute

Play Episode Listen Later Mar 5, 2020 12:47

Discussion of normalization (there is some way to reach a normal form) versus termination (no matter how you execute the term you reach a normal form). A little more discussion of strong FP. For type theory, the need for normalization due to Curry-Howard and due to conversion checking.

conversion fp normalization curry howard

Why go beyond GADTs?

Iowa Type Theory Commute

Play Episode Listen Later Jan 24, 2020 12:25

GADTs are quite powerful. Why go all the way to true dependent types? And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcast) or not?

go beyond curry howard

Episode 3 - Partial Application (not Currying)

Programming

Play Episode Listen Later Jan 13, 2020 9:05

Today we'll discuss partial application and currying. By the end of the episode, you'll understand what these two different concepts are how they are different from each other, and where you can apply them in practice. In between the episode, we'll also talk about the brilliant computer scientist Haskell Curry, and we'll mention the Curry-Howard isomorphism

application partial currying curry howard

Program Termination and the Curry-Howard Isomorphism

Iowa Type Theory Commute

Play Episode Listen Later Jan 10, 2020 10:57

For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type. Under Curry-Howard this means any formula is provable, which is one way to define inconsistency. (And logics have to be consistent to be useful.)

termination curry howard

Why Curry-Howard for classical proofs is a bad idea for programming

Iowa Type Theory Commute

Play Episode Listen Later Jan 6, 2020 14:09

If you have dependent types, classical reasoning, and the Curry-Howard isomorphism, you can write programs that look like they are invoking oracles for undecidable problems -- but they are not, and this is confusing.

programming classical bad idea proofs curry howard

Curry-Howard for classical logic

Iowa Type Theory Commute

Play Episode Listen Later Jan 6, 2020 11:58

CH can be applied to classical logic, too. The seminal paper is A Formulae-as-Types Notion of Control by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.

logic classical formula e curry howard