Type Theory 公開
[search 0]
もっと

Download the App!

show episodes
 
Type Theory Forall is a podcast hosted by Pedro Abreu, a Purdue PhD Student in Programming Languages. Our goal is to bridge the gap between academia and the world of Programming Languages and Type Theory. For this we interview professors, students and anyone who seem to have something relevant to share about the state of the art of Programming Languages Research.
 
Loading …
show series
 
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.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…
 
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).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 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.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 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…
 
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...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.…
 
In this episode we host a discussion between Anupam Das and ThorstenAltenkirch on the role of constructivism in mathematics, logic and computerscience. Anupam is a lecturer in the University of Birmingham in the UK, and ThorstenAltenkirch is a CS Professor at the University of Nottingham. We discuss why constructive content in proofs matters, the l…
 
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…
 
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.…
 
In a really wonderful paper of some few years back, Swierstra introduced the idea of modular datatypes using ideas from universal algebra. Modular datatypes allow one to assemble a bigger datatype from component datatypes, and combine functions written on the component datatypes in a modular way. In this episode I introduce the paper and the proble…
 
In a 2013 journal article titled "A Scalable Module System", Florian Rabe and Michael Kohlhase propose a module system called MMT (Modules for Mathematical Theories) for structuring mathematical knowledge. The paper has a very interesting general discussion of module systems, from programming languages but also other areas like algebraic specificat…
 
In this episode I interview Anupam Das we have a nice conversation on thehistorical perspective of how Logic and Proof Theory as we know today cameabout in the 30’s. The differences between Natural Deduction and SequentCalculus, Cut Elimination and much more. Links Anupam Das The Proof Theory Blog Stanford Encyclopedia of Philosophy Anupam’s Talk o…
 
I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my mind about these. I also mention a few other languages' module systems (Clojure, Java 9). I also ponder names and namespace management.Aaron Stump による
 
In this episode I have a nice conversation with Chris Jenkins to talk aboutthe Cedille theorem prover, based on a very concise type theory called CDLE.The main selling point of Cedille is that the theory is so small that thetyping rules fit one page. And yet it is strong enough to do relevant theoremproving. This is probably the most technical epis…
 
SML has arguably the most complicated/powerful module system of any existing programming language. It is a luxury RV to Haskell's camper van. I take a high-level look, following a very nice paper by Xavier Leroy, titled "A modular module system".Aaron Stump による
 
I start Chapter 13 (in Season 2) of the podcast, on module systems. Almost all programming languages I know include some kind of scheme for modules, packages, namespaces, or something like this. I discuss the high-level ideas of namespace management and type abstraction, two main use cases for module systems. Subsequent episodes will discuss module…
 
In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some time hacking on its internals. Me and Daniel also talk about Mizar, Isar, the seL4, and how it is formalized. Torwards the end of the episode we also talk a little about his current work on the binary analysis…
 
In this episode we interview Zeina Migeed, a PhD Student at University ofCalifornia Los Angeles, advised by Prof. Jens Palsberg She Researches Gradual Types and had a paper published at POPL’20 named “What isDecidable about Gradual Types”. here is a link to it As the name of the episode suggests, I’ll be asking her all the dumb questionsrelated to …
 
I discuss the perhaps surprising fact that union and intersection types are quite actively used and promoted for languages like TypeScript, also OO languages like Scala. I also try to explain briefly a counterexample to type preservation with union types, which you can find at the start of Section 2 of Barbanera and Dezani-Ciancaglini's paper "Inte…
 
I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion. Hence any normalizing term is typable (since it reduces to a n…
 
In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept. Links: Yves email: yves.bertot@inria.fr Affichage et manipulation interactive de formules mathématiques dan…
 
Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is closed under beta-reduction. With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normal…
 
In this episode we host Eric Bond to go through some real cool projectshappening in the PL World and some of the companies behind them. We discuss some technical differences between the major interactive theoremprovers out there, some of their most popular projects, and a fewcompanies that work in the realm. Eric Bond works at 47 degrees, a consult…
 
In this episode we host Dan Zheng, an alumni of Purdue University that nowworks at Google at real cool projects that relates ML and PL. We chat about how was his transition from undergrad to such a huge companylike Google. We talk about cool languages such as Lantern, LLVM, LMS, Julia, Rust, Racket, Scala. How does ML and PL can be used to enhance …
 
Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), RelTT instead has a refinement of this called Identity Inclusion. Instead of saying that the interpretation of every closed type is the identity relation (…
 
I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.…
 
In this episode we host Rajan Walia and John Sarracino. Rajan is a last yearPhD Student from Indiana University, working under Sam Tobin-Hochstadt. AndJohn is a Postdoc working with Greg Morriset at Cornell University. We talk about Grad School life, how academia life looks like,pressure to publish, work-life balance, industry vs academia, and much…
 
I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.Aaron Stump による
 
In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research: What is PL research? Why does it matter? Why is it cool? What is Lambda Calculus? What is Type Theory? Church-Turing Thesis? Curry-Howard Correspondence? What are proof assistants? Why are they cool? Don’t…
 
This episode continues the introduction of RelTT by presenting the types of the language. Because the system is based on binary relational semantics, we can include binary relational operators like composition and converse as type constructs! Strange. The language also promotes terms to relations, by viewing them as functions and then taking their …
 
This episode begins Chapter 11 of the podcast, on Relational Type Theory. This is a new approach to type theory that I am developing. The idea is to design a type system based on the binary relational semantics for types, which we considered in Chapter 10. This episode recalls some of that semantics.…
 
Who is Pedro Abreu? What is the goal of this Podcast? What are My Research Interests? In this episode I share about my internship experiences at Nicta (data61 now), Sifive, Galois and Nomadic Labs. Welcome! Don’t forget to checkout Galois’ new podcast hosted by Joey Dodds and ShapatMorina. Click Here…
 
In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Parametric Polymorphism" by the great John C. Reynolds. I summarize the two interconnected semantics for polymorphic types proposed by Reynolds: one which interprets types as sets and programs as members of those s…
 
Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence. This is a feature of a type theory where different implementations of the same interface can be proved equivalent, and used interchangeably in the theory. Only in the past couple years have researcher…
 
Loading …

クイックリファレンスガイド

Google login Twitter login Classic login