Type Theory 公開
[search 0]
もっと

Download the App!

show episodes
 
Loading …
show series
 
In this episode we partner with Formal Land, a company that works in formallyverifying the Tezos codebase! I have worked with them in the past developingnew features to their source-to-source compiler CoqOfOcaml. In this episode wetalk about their work with Tezos and how their techniques are applicable toother codebases as well! For this we talk wi…
 
In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart contract, using their K-Michelson tool, which provides an executable description of the operational semantics of the Michelson language used for smart contracts on the Tezos blockchain.…
 
In this episode we interview Lawrence Paulson, one of the creating fathers ofIsabelle. We talk about the development process, how it drew inspirations andideas from LCF and Boyer Moore. What tools were used, it’s strenghts andweaknesses, and all about the historical context at the time! We also brieflytalk about his formalization of the Gödel’s Inc…
 
In this episode we talk about Sigplan, the organization behind the mostimportant conferences and proceedings in our field. What is the SIGPLAN? Whatexactly does it do? How is it organized? How are things published? To answerthese and many other questions we talk with Jens Palsberg, a professor atUCLA, who is the past chair of the SIGPLAN. And also …
 
In this episode Cody Roux teaches some interesting concepts that people careabout in Mathematics and Logic as a way to try to understand what is going onin the universe around us! In particular we will try to explain concepts suchas Impredicativity, Excluded Middle, Group Theory, Model Theory, KripkeModels, Realizability, The Markov Principle, Cut …
 
In this episode Conal Elliott gives a more concrete presentationon what is Denotational Design is and how to use it in practice. It is a continuation of episode #17, in which we had an in-depth philosophicalconversation to explain why he believes thatDenotational Design is a superior form of reasoning in the realm of computerscience. We also contin…
 
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.…
 
In this episode, me and Eric Bond have a great conversation with Dan R.Ghica, a professor at Birmingham University and Director of the ProgrammingLanguage Research Lab of the Huaweii Research Centre Edinburgh. We talk about his work on both institutions, which includes topics such asCategory Theory, String Diagrams, and Game Semantics. We also brie…
 
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…
 
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…
 
In today’s episode I invite two friends of mine Patrick Lafontaine and SupunAbeysinghe. We will talk about their experience learning Coq and we guideourselves in a survey that I gave all the 83 students in the class.The class was thought by my advisor Benjamin Delaware and I was his TA. Patrick researches compilers and have done work in particular …
 
In this episode Cody Roux talks about the Gödel’s Incompleteness Theorems. We gothrough it’s underlying historical context, Hilbert’s Program, how it relateswith Turing, Church, Von Neumann, Termination and more. Links Cody’s website Cody’s dblp The Lady or the Tiger? - Short Story The Lady or the Tiger? - Amazon Logicomix An Introduction to Gödel’…
 
In this episode I had the pleasure to have an in-depth conversation with ConalElliott about his life, his work, his philosophy and his many opinions aboutresearch and the current state of PL Research and how it lead him to come withthe concept of Denotational Design. Conal got his PhD at CMU in the 90s underFrank Pfenning working on Higher-Order Un…
 
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 …
 
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…
 
in this episode we interview Jesper Cockx, one of the core developers on Agda.We talk about the philosophy behind Agda, his work on pattern matching, theUniqueness of Identity of Proofs, UIP for short, and why it is inconsistentwith Homotopy Type Theory. Links Jesper’s Website Jesper’s Twitter: @agdakx Jesper’s PhD Thesis Rewrite Theory paper Patte…
 
In this episode me, Eric and Nitin continues our conversation started in thelast episode. This time we move our attention to the cool projects happeningin Coq, in particular commenting through the projects mentioned in AndrewAppel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” thattook place in CPP’22 which is colocated with POPL …
 
In this episode I gather with two good friends Eric and Nitin to randomly talk random subjects that pops up. Among them we talked about POPL, Scala, Isabelle, Parametricity, Dependent Object Types (DOT, for short) and more! Links Nitin Twitter @NitinJohnRaj2 Eric Twitter @EricBond10 Collection of links on logical relations Theorems for Free Reynold…
 
This episode is about the journey of a programmer that converted himself intoa Haskell developer after working with C/C++ for more than 10years. Here are a few questions that you’ll find the answer to in this episode: What does he find so compelling about Haskell? Why did it make him dive deeper into the Theoretical Computer Science? Why did it mak…
 
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.Aaron Stump による
 
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…
 
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…
 
Talia Ringer is an Assistant Professor at University of IllinoisUrbana-Champaign. She did her PhD at University of Washington with her thesison Proof Repair. She’s very active on twitter @taliaringer. And in this episode we will talkabout her transition from PhD to Professor, her work on diversity, her ADHD andhow it has affected her career so far,…
 
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 による
 
In this episode we have talk with Alejandro Serrano Mena, heworks on 47 degrees and is a published author of two books about Haskell: TheBook of Monads and Practical Haskell. We talk about many interesting features behind functionalprogramming such as adts, pattern matching, impredicativity, monads, effects,hacking the ghc and how all this comes to…
 
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 …
 
Loading …

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

Google login Twitter login Classic login