Iowa Type Theory Commute podcast

Player FM - Internet Radio Done Right

17 subscribers

تمت الإضافة منذ قبل five أعوام

المحتوى المقدم من Aaron Stump. يتم تحميل جميع محتويات البودكاست بما في ذلك الحلقات والرسومات وأوصاف البودكاست وتقديمها مباشرة بواسطة Aaron Stump أو شريك منصة البودكاست الخاص بهم. إذا كنت تعتقد أن شخصًا ما يستخدم عملك المحمي بحقوق الطبع والنشر دون إذنك، فيمكنك اتباع العملية الموضحة هنا https://ar.player.fm/legal.

This Is Woman's Work with Nicole Kalil

1
Grown-Up Goals: The 5 Pillars Of Being A Healthy Adult with Michelle Chalfant | 317 35:24

منذ 7 أيام35:24

التشغيل لاحقا

قوائم

إعجاب

احب

35:24

Let’s talk about adulting— actual adulting. Not just paying bills or keeping a houseplant alive, but the kind that involves emotional maturity, healthy boundaries, and conscious self-leadership. Because let’s be honest, most of us weren’t taught how to be fully functioning adults… and it shows. Joining us is Michelle Chalfant , licensed therapist turned holistic life coach, creator of The Adult Chair® model, and author of the new book The Adult Chair: Get Unstuck, Claim Your Power, and Transform Your Life . With millions reached through her podcast, coaching programs, and retreats, she’s here to walk us through the five pillars of being a healthy, grounded adult. Here’s the truth: being an adult isn’t about checking boxes or pretending you’re fine. It’s about owning your truth. Feeling your feelings. Practicing compassion without letting yourself off the hook. It’s about setting firm boundaries—with no need for justification—and recognizing that your triggers are not flaws, they’re clues. None of us were handed a guidebook for how to grow up emotionally. We inherited patterns from people who were figuring it out as they went. But what Michelle shares today is empowering: it’s never too late to unlearn what no longer serves you and become the adult you were meant to be. Whether you’re starting this work or knee-deep in your personal development era, this episode will meet you where you are—and help you move forward with clarity, self-trust, and strength. Connect with Michelle: Website: https://theadultchair.com/ Book: https://theadultchair.com/book IG: https://www.instagram.com/themichellechalfant/?hl=en FB: https://www.facebook.com/@TheMichelleChalfant/ YouTube: https://www.youtube.com/c/michellechalfant Related Podcast Episodes: How To Build Emotionally Mature Leaders with Dr. Christie Smith | 272 Boundaries vs. Ultimatums with Jan & Jillian Yuhas | 297 Gentleness: Cultivating Compassion for Yourself and Others with Courtney Carver | 282 Share the Love: If you found this episode insightful, please share it with a friend, tag us on social media, and leave a review on your favorite podcast platform! 🔗 Subscribe & Review: Apple Podcasts | Spotify | Amazon Music Learn more about your ad choices. Visit megaphone.fm/adchoices…

Iowa Type Theory Commute

منزل السلاسل•Feed

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

175 حلقات

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

Iowa Type Theory Commute

17 subscribers

updated منذ عام واحد

منزل السلاسل•Feed

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

175 حلقات

#Science #Tech #Math #Aaron Stump #Programming Language #Computational Logic #Type Theory #Proof Assistants #Cedille

كل الحلقات

Iowa Type Theory Commute

1
Correction: the Correct Author of the Proof from Last Episode, and an AI flop 7:10

منذ 5 weeks7:10

7:10

I correct what I said in the last episode about the author of the proof of FD from last episode based on intersection types. I also describe AI flopping when I ask it a question about this.

Iowa Type Theory Commute

1
Krivine's Proof of FD, Using Intersection Types 21:35

منذ 6 weeks21:35

21:35

Krivine's book (Section 4.2) has a proof of the Finite Developments Theorem, based on intersection types. I discuss this proof in this episode.

Iowa Type Theory Commute

1
A Measure-Based Proof of Finite Developments 23:24

منذ 9 weeks23:24

23:24

I discuss the paper "A Direct Proof of the Finite Developments Theorem" , by Roel de Vrijer. See also the write-up at my blog.

Iowa Type Theory Commute

1
Introduction to the Finite Developments Theorem 15:54

منذ 12 weeks15:54

15:54

The finite developments theorem in pure lambda calculus says that if you select as set of redexes in a lambda term and reduce only those and their residuals (redexes that can be traced back as existing in the original set), then this process will always terminate. In this episode, I discuss the theorem and why I got interested in it.…

Iowa Type Theory Commute

1
Nominal Isabelle/HOL 16:18

منذ 20 weeks16:18

16:18

In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL , by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.

Iowa Type Theory Commute

1
The Locally Nameless Representation 19:54

منذ 24 weeks19:54

19:54

I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction. I also answer a listener's question about what "computational type theory" means. Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.…

Iowa Type Theory Commute

1
POPLmark Reloaded, Part 1 15:14

منذ 25 weeks15:14

15:14

I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations , which proposes a benchmark problem for mechanizing Programming Language theory.

Iowa Type Theory Commute

1
POPLmark Reloaded, Part 2 13:59

منذ 25 weeks13:59

13:59

I continue the discussion of POPLmark Reloaded , discussing the solutions proposed to the benchmark problem. The solutions are in the Beluga, Coq (recently renamed Rocq), and Agda provers.

Iowa Type Theory Commute

1
Introduction to Formalizing Programming Languages Theory 12:20

منذ 29 weeks12:20

12:20

In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.

Iowa Type Theory Commute

1
Turing's proof of normalization for STLC 17:39

منذ 1 year17:39

17:39

In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing's original proof and some historical comments.

Iowa Type Theory Commute

1
Introduction to normalization for STLC 9:39

منذ 1 year9:39

9:39

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).…

Iowa Type Theory Commute

1
Arithmetic operations in simply typed lambda calculus 9:56

منذ 1 year9:56

9:56

It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A. Interestingly, things change with exponentiation, which we will consider in the next episode.…

Iowa Type Theory Commute

1
The curious case of exponentiation in simply typed lambda calculus 7:29

منذ 1 year7:29

7:29

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surprisingly, the type is non-uniform. If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A. The second argument needs to have type at strictly higher order than the first argument. This has the fascinating consequence that we cannot define self-exponentiation, \ x . exp x x. That term would reduce to \ x . x x, which is provably not typable in STLC.…

Iowa Type Theory Commute

1
More on basics of simple types 15:45

منذ 1 year15:45

15:45

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

Iowa Type Theory Commute

1
Begin Chapter on Simple Type Theory 15:41

منذ 1 year15:41

15:41

In this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some basic examples. Subsequent episodes will discuss various interesting nuances...

مرحبًا بك في مشغل أف ام!

يقوم برنامج مشغل أف أم بمسح الويب للحصول على بودكاست عالية الجودة لتستمتع بها الآن. إنه أفضل تطبيق بودكاست ويعمل على أجهزة اندرويد والأيفون والويب. قم بالتسجيل لمزامنة الاشتراكات عبر الأجهزة.