160 Folgen

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

Iowa Type Theory Commute Aaron Stump

    • Technologie

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

    Some advanced examples in DCS

    Some advanced examples in DCS

    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 linear time.  I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.

    • 23 Min.
    DCS compared to termination checkers for type theories

    DCS compared to termination checkers for type theories

    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. 

    • 19 Min.
    Getting started with DCS

    Getting started with DCS

    In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute!  The repo is here.

    • 17 Min.
    Introduction to DCS

    Introduction to DCS

    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 this basic design, and its rationale.  

    • 11 Min.
    Semantics of subtyping

    Semantics of subtyping

    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 comparison of the two kinds of subtyping.  With coercive subtyping, we have subtyping axioms "A : B by c", where c is a function from A to B.  The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be converted to one of type B.  Subsumptive subtyping says that A : B means that the meaning of A is a subset of the meaning of B.  So this kind of subtyping depends on a semantics for types.  A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants.  So a type like Integer might be interpreted as the set of all integers, etc.  Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms.  For in that situation, A : B does not imply List A : List B, because Nil A is an inhabitant of List A but not of List B (which requires instead Nil B).

    Join the telegram group here.

    • 15 Min.
    More on type inference for simple subtypes

    More on type inference for simple subtypes

    I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes.  Coming soon: a discussion of semantics of subtyping.

    • 9 Min.

Top‑Podcasts in Technologie

Lex Fridman Podcast
Lex Fridman
Darknet Diaries
Jack Rhysider
Ö1 Digital.Leben
ORF Ö1
Mac & i - der Apple-Podcast
Mac & i
Flugforensik - Abstürze und ihre Geschichte
Flugforensik
Hard Fork
The New York Times

Das gefällt dir vielleicht auch