Iowa Type Theory Commute
Iowa Type Theory Commute
Episodes
Episodes of Iowa Type Theory Commute
Mark All
I discuss the paper "A Direct Proof of the Finite Developments Theorem", by Roel de Vrijer. See also the write-up at my blog.
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 wi
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
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
I discuss the paper POPLmark Reloaded: Mechanizing Proofs by Logical Relations, which proposes a benchmark problem for mechanizing Programming Language theory.
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.
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.
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.
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
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 exponentia
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
I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
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...
This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in li
In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.
In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.
DCS is a new functional programming language I am designing and implementing with Stefan Monnier. DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation. In this episode, I talk about
I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a compar
I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.
In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make type
In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus. I mostl
In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.
We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very usef
In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which us
I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality
Unlock more with Podchaser Pro
- Audience Insights
- Contact Information
- Demographics
- Charts
- Sponsor History
- and More!
- Account
- Register
- Log In
- Find Friends
- Resources
- Help Center
- Blog
- API
Podchaser is the ultimate destination for podcast data, search, and discovery. Learn More
- © 2025 Podchaser, Inc.
- Privacy Policy
- Terms of Service
- Contact Us