Cedille is a not-for-profit record label dedicated to extraordinary classical music and the brilliant artists who create it. We enhance the world's catalog of recorded music through audiophile-quality recordings featuring Chicago's finest musicians. Each episode of Cedille's Classical Chicago Podcast highlights a new release and feature interviews with your favorite Cedille artists. To support Cedille and its mission, please visit CedilleRecords.org

C

Cedille Records

###
1
Episode 56 – Joel Link / Beethoven Complete String Quartets: Volume 3 — The Late Quartets
1:10:48

1:10:48

Play later

Play later

Lists

Like

Liked

1:10:48
On this episode of Classical Chicago, Cedille President Jim Ginsburg talks with the Dover Quartet's Joel Link about the chamber group's album "Beethoven Complete String Quartets: Volume 3 — The Late Quartets." This triple-CD release comprises Beethoven’s very last compositions — remarkable and often daunting works that upended the concept of the st…

I

Iowa Type Theory Commute

###
1
Separation Logic II: recursive predicates
11:52

11:52

Play later

Play later

Lists

Like

Liked

11:52
I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data structure using separating conjunction and recursive predicates.By Aaron Stump

C

Cedille Records

###
1
Episode 55: Rachel Barton Pine / Violin Concertos by Black Composers Through the Centuries
1:31:00

1:31:00

Play later

Play later

Lists

Like

Liked

1:31:00
On this episode of Classical Chicago, Cedille President Jim Ginsburg talks with violinist Rachel Barton Pine about Violin Concertos by Black Composers Through the Centuries: 25th anniversary edition. The album features Pine's new recording of Florence Price's Violin Concerto No. 2, with the Royal Scottish National Orchestra & Jonathon Heyward, and …

C

Cedille Records

###
1
Episode 54: Julian Velasco / As We Are
1:39:46

1:39:46

Play later

Play later

Lists

Like

Liked

1:39:46
On this episode of Classical Chicago, Cedille President Jim Ginsburg converses with saxophonist Julian Velasco, winner of Cedille Records' first-ever Emerging Artist Competition, about his upcoming debut album, As We Are.By Cedille Records

I discuss separation logic, as presented in this seminal paper by the great John C. Reynolds. I did not go very far into the topic, so please expect a follow-up episode.By Aaron Stump

In this episode, I talk briefly about Rust, which uses compile-time analysis to ensure that code is memory-safe (and also free of data races in concurrent code) without using a garbage collector. Fantastic! The language draws on but richly develops ideas on ownership that originated in academic research.…

C

Cedille Records

###
1
Episode 53 - Aurelien Fort Pederzoli (Black Oak Ensemble) / Avant l'orage
1:34:41

1:34:41

Play later

Play later

Lists

Like

Liked

1:34:41
Episode 53 - Aurelien Fort Pederzoli (Black Oak Ensemble) / Avant l'orage by Cedille RecordsBy Cedille Records

I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to declare explicitly the region from which to satisfy individual allocation requests. Regions are created in a statically scoped way, so that after execution leaves the body of the region-creation construct, the ent…

I

Iowa Type Theory Commute

###
1
Introduction to verified memory management
17:08

17:08

Play later

Play later

Lists

Like

Liked

17:08
In this episode, I start a new chapter (we are up to Chapter 16, here), about verifying safe manual management of memory. I have personally gotten pretty interested in this topic, having seen through some simple experiments with Haskell how much time can go into garbage collection for seemingly simple benchmarks. I also talk about why verifying mem…

C

Cedille Records

###
1
Episode 52 - David Cunliffe (Lincoln Trio) / Trios From Contemporary Chicago
1:03:10

1:03:10

Play later

Play later

Lists

Like

Liked

1:03:10
Episode 52 - David Cunliffe (Lincoln Trio) / Trios From Contemporary Chicago by Cedille RecordsBy Cedille Records

I laud the Metamath proof checker and its excellent book. I am also looking for suggestions on what to discuss next, as I am ready to wrap up this chapter on proof assistants.By Aaron Stump

In this episode I share my initial impressions -- very positive! -- of the Metamath system. Metamath allows one to develop theorems from axioms which you state. Typing or other syntactic requirements of axioms or theorems are also expressed axiomatically. The system exhibits an elegant coherent vision for how such a tool should work, and was super …

C

Cedille Records

###
1
Episode 51 - Robert Dillon (Third Coast Percussion) / Perspectives
1:19:47

1:19:47

Play later

Play later

Lists

Like

Liked

1:19:47
Episode 51 - Robert Dillon (Third Coast Percussion) / Perspectives by Cedille RecordsBy Cedille Records

I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for formalized proofs of the irrationality of the square root of 2. The book was published in 2006, and made an impression on me then. The provers we have discussed so far all have a solution in the book, except for…

C

Cedille Records

###
1
Episode 50: Ani & Marta Aznavoorian / Gems from Armenia
1:06:25

1:06:25

Play later

Play later

Lists

Like

Liked

1:06:25
Episode 50: Ani & Marta Aznavoorian / Gems from Armenia by Cedille RecordsBy Cedille Records

I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.By Aaron Stump

In this episode, I talk about what I have learned so far about the Lean prover, especially from an excellent (if somewhat advanced) Master's thesis, "The Type Theory of Lean" by Marco Garneiro.By Aaron Stump

I

Iowa Type Theory Commute

###
1
More on Isabelle, and the Complexity of ITPs
16:14

16:14

Play later

Play later

Lists

Like

Liked

16:14
I talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.By Aaron Stump

C

Cedille Records

###
1
Episode 49 - Alex Klein / When There Are No Words
1:24:41

1:24:41

Play later

Play later

Lists

Like

Liked

1:24:41
Episode 49 - Alex Klein / When There Are No Words by Cedille RecordsBy Cedille Records

The Isabelle theorem prover supports different logics, but its most developed seems to be Higher-Order Logic (HOL). In this episode, I talk about the logic and approach of Isabelle/HOL, as far as I have understood them.By Aaron Stump

I talk a bit more about the Agda proof assistant.By Aaron Stump

In this episode I talk a bit about the Agda proof assistant.By Aaron Stump

I talk about a couple good resources for learning Coq, the problem of too many ways to do things in type theory, and issues trying to explain and document a very complex language.By Aaron Stump

I discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.By Aaron Stump

I

Iowa Type Theory Commute

###
1
Introduction to Interactive Theorem Provers
11:58

11:58

Play later

Play later

Lists

Like

Liked

11:58
This is the start of Chapter 15, about interactive theorem provers (ITPs). In this episode, I talk about the difference between fully automatic and interactive provers, and my plan to discuss and compare several different ITPs, in future episodes of this chapter.By Aaron Stump

I

Iowa Type Theory Commute

###
1
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
14:10

14:10

Play later

Play later

Lists

Like

Liked

14:10
In this episode, I outline the argument for why the proof-theoretic ordinal (in the sense of Rathjen, as presented last episode) is epsilon-0. My explanation has something of a hole, in explaining how one would go about deriving induction for ordinals strictly less than epsilon-0 in Peano Arithmetic. To help paper over this hole a little, I discuss…

I

Iowa Type Theory Commute

###
1
The proof-theoretic ordinal of a logical theory
12:14

12:14

Play later

Play later

Lists

Like

Liked

12:14
Ordinal analysis seeks to determine the strength of a logical theory by assigning an ordinal to it. Which one? In this episode I describe a definition of the proof-theoretic ordinal of a logical theory from a paper by proof theorist Michael Rathjen. It is basically a measure of how strong an induction principle is derivable in the theory. (The firs…

Ordinal analysis is an important branch of proof theory, which seeks to compare, quantitatively, the strengths of different proof systems. The quantities in question are ordinals, which extend the ordering character of natural numbers into the infinite. In this episode, I discuss these ideas a bit further, and also review a little the ordinals up t…

I

Iowa Type Theory Commute

###
1
An analogy for multiplicative disjunction
11:24

11:24

Play later

Play later

Lists

Like

Liked

11:24
Listen in while I have an actual insight on air! After a week of head scratching, I figure out -- while chattering! -- what I hope is both a correct and intuitive example of multiplicative disjunction.By Aaron Stump

I explain the basic idea of multiplicative versus additive proof rules, and consider multiplicative conjunction (tensor), addition conjunction (&, "with"), additive disjunction -- but leaving multiplicative disjunction (par) for next time!By Aaron Stump

We discuss briefly the central ideas of linear logic, where by default assumptions must be used exactly once.By Aaron Stump

C

Cedille Records

###
1
Episode 48 - Anthony McGill & Gloria Chien / Here With You
1:14:28

1:14:28

Play later

Play later

Lists

Like

Liked

1:14:28
Episode 48 - Anthony McGill & Gloria Chien / Here With You by Cedille RecordsBy Cedille Records

I

Iowa Type Theory Commute

###
1
Structural rules, or the Curse of the Bound Variable
12:55

12:55

Play later

Play later

Lists

Like

Liked

12:55
In this episode I discuss the basic structural rules of weakening, contraction, and exchange, and speculate on their dark origin.By Aaron Stump

I

Iowa Type Theory Commute

###
1
Why Cut Elimination is More Complicated than Normalization
12:06

12:06

Play later

Play later

Lists

Like

Liked

12:06
Cut elimination for sequent calculus is more involved that normalization of detours for natural deduction. There are more cases of cuts that must be transformed than correspond to detours (introductions followed by eliminations). In this episode, I explain why that is.By Aaron Stump

We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula. What corresponds to this for sequent calculus proofs? The answer is cut elimination. This episode describes the cut rule and…

C

Cedille Records

###
1
Episode 47 - Camden Shaw (Dover Quartet) / Beethoven Complete String Quartets Vol 2
1:21:55

1:21:55

Play later

Play later

Lists

Like

Liked

1:21:55
Episode 47 - Camden Shaw (Dover Quartet) / Beethoven Complete String Quartets Vol 2 by Cedille RecordsBy Cedille Records

I

Iowa Type Theory Commute

###
1
Normalization of detours for implication inferences
12:48

12:48

Play later

Play later

Lists

Like

Liked

12:48
We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implication rules. Under Curry-Howard, this actually corresponds to beta-reduction, and could make the proof bigger (though less complex in a certain sense).By Aaron Stump

This episode explains the idea of normalization of proofs in natural deduction. We want to eliminate so-called detours in proofs, which occur when an introduction is immediately followed by an elimination.By Aaron Stump

Sequent calculus is a different style in which proof systems can be formulated, where for each connective, we have a left rule for introducing it (in the conclusion of the rule) in the left part of a sequent G => D (i.e., in G), and similarly a right rule for introducing it in the right part (D). The beauty of sequent calculus is disjunction is han…

We discuss further inferences in natural deduction, in particular implication introduction and elimination.By Aaron Stump

We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences. It is a research problem to fix this! Don't forget to get in touch with me if you want to do the mini-course over Zoom next month, on normalization.By Aaron Stump

This episode begins the discussion of the style of proof known as Natural Deduction, invented by Gerhard Gentzen, a student of Hermann Weyl, himself a student of David Hilbert (sorry, I said incorrectly that Gentzen was Hilbert's own student). Each logical connective (like OR, AND, IMPLIES, etc.) has introduction rules that let you prove formulas b…

We continue our gradual entry into proof theory by talking about reflecting meta-logical reasoning into logical rules, and naming the three basic proof systems (Hilbert-style, natural deduction, and sequent calculus). Advertising for the October 3-session Zoom mini-course on normalization continues. Email me if you are interested! This is just for …

I

Iowa Type Theory Commute

###
1
Different proof systems, distinguishing logical rules from domain axioms
12:02

12:02

Play later

Play later

Lists

Like

Liked

12:02
I highlight two basic points in this continuing warm-up to proof theory: there are different proof systems for the same logics, and it is customary to separate purely logical rules (dealing with propositional connectives and quantifiers, for example) from rules or axioms for some particular domain (like axioms about arithmetic, or whatever domain i…

I

Iowa Type Theory Commute

###
1
Introduction to Proof Theory (Start of Season 3)
18:17

18:17

Play later

Play later

Lists

Like

Liked

18:17
This is the start of Season 3 of the podcast. We are beginning with a new chapter (Chapter 14) on Proof Theory. This episode gives some basic introduction to the history and broad concerns of proof theory. There is even music, composed and played by yours truly, chez nous...By Aaron Stump

In this episode I discuss the paper "Modula-2 and Oberon" by Niklaus Wirth. Modula-2 introduced (it seems from the paper) the idea of having modules with explicit import and import lists -- something we saw at the start of our look at module systems with Haskell's module system. I note some interesting historical points raised by the paper.…

C

Cedille Records

###
1
Episode 46 - Andy Baker & Anthony Devroye / Leo Sowerby: The Paul Whiteman Commissions...
1:29:52

1:29:52

Play later

Play later

Lists

Like

Liked

1:29:52
Episode 46 - Andy Baker & Anthony Devroye / Leo Sowerby: The Paul Whiteman Commissions... by Cedille RecordsBy Cedille Records

Analogously to the decomposition of a datatype into a functor (which can be built from other functors to assemble a bigger language from smaller pieces of languages) and a single expression datatype with a sole constructor that builds an Expr from an F Expr (where F is the functor) -- analogously, a recursion can be decomposed into algebras and a f…

I

Iowa Type Theory Commute

###
1
Reassembling datatypes from functors using a fixed-point
10:16

10:16

Play later

Play later

Lists

Like

Liked

10:16
Last episode we discussed how functors can describe a single level of a datatype. In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype. The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described …

This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the application of a fixed-point type constructor and then a functor. The functor itself can be assembled from other functors for pieces of the datatype. This makes modular datatypes possible.…