Podcasts about type theory

Andrej Bauer has done his PhD at CMU under Dana Scott, and he stands right on the edge between mathematics and computer science. During our conversation it just feels that he can just go on in depth about any topic remotely related to Type Theory and Programming Languages. Andrej is the person who organized for the The Proof Assistants stack exchange. He has an incredible blog that's always a great resource to learn Type Theory and Programming Languages Theory. He also has an incredible series of summer school lectures on effect handlers. But more specifically today we talk about Constructivism, Dialectica, Effect Handlers and AI. I'm sure you guys are gonna love it! Links Andrej's Website Andrej's Blog

In this episode we talk with Nicolas Tabareau, the Head of Gallinette, one of the main teams which develop the Rocq theorem Prover at Inria. The original idea of this interview is to talk about the rebranding from Coq into Rocq, which is very exciting to our community. However, Nicolas has such a prolific research career that I couldn't miss the opportunity to get him to talk so much more about it. So in this conversation we talk about his early publications in neuroscience, his views on Category Theory applied to Type Theory, Rocq's rebranding, and the institution around it, MetaRocq and the conceptual boundaries of certifying a theory inside itself. Of course we wouldn't miss the opportunity to also discuss how Rocq view the growing influence that Lean is gaining in our community. Links Type Theory Forall Store Type Theory Forall Website Nicolas Tabareau Website MetaRocq Github

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 Pierre-Marie Pédrot who is one of the main Coq/Rocq developers joins us to talk about what is Type Theory, what is Martin-Löf Type Theory, what are the properties we should care about in our type theory and why. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall Links Pierre-Marie's Website Type Theory Forall website Type Theory Forall discord

Dr. Eric Daimler is a leading authority in robotics and artificial intelligence with over 20 years of experience as an entrepreneur, investor, technologist, and policymaker. He served as a Presidential Innovation Fellow for AI and Robotics under the Obama Administration, driving U.S. leadership in AI research and commercialization. Eric has founded and led several pioneering tech companies and currently serves on the boards of WelWaze Medical and Petuum. His latest venture, Conexus, addresses the critical issue of data deluge in information technology. With a career spanning business, academia, and policy, Eric offers a unique perspective on shaping the future of AI for societal benefit.  00:00 Snippet01:09 Our Guest05:40 AI is much more than Machine Learning10:57 Lisp and data30:54 Conexus 32:53 Type Theory and Quantum compiling34:44 The government's role in AI39:14 Connecting with Eric ------------------------------------------------------------------ To learn more about Eric visit https://www.linkedin.com/in/ericdaimler/ To learn more about Dark Rhiino Security visit https://www.darkrhiinosecurity.com ------------------------------------------------------------------ SOCIAL MEDIA: Stay connected with us on our social media pages where we'll give you snippets, alerts for new podcasts, and even behind the scenes of our studio! Instagram: @securityconfidential and @Darkrhiinosecurity Facebook: @Dark-Rhiino-Security-Inc Twitter: @darkrhiinosec LinkedIn: @dark-rhiino-security Youtube: @DarkRhiinoSecurity ​

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...

It's the Season 10 finale of the Elixir Wizards podcast! José Valim, Guillaume Duboc, and Giuseppe Castagna join Wizards Owen Bickford and Dan Ivovich to dive into the prospect of types in the Elixir programming language! They break down their research on set-theoretical typing and highlight their goal of creating a type system that supports as many Elixir idioms as possible while balancing simplicity and pragmatism. José, Guillaume, and Giuseppe talk about what initially sparked this project, the challenges in bringing types to Elixir, and the benefits that the Elixir community can expect from this exciting work. Guillaume's formalization and Giuseppe's "cutting-edge research" balance José's pragmatism and "Guardian of Orthodoxy" role. Decades of theory meet the needs of a living language, with open challenges like multi-process typing ahead. They come together with a shared joy of problem-solving that will accelerate Elixir's continued growth. Key Topics Discussed in this Episode: Adding type safety to Elixir through set theoretical typing How the team chose a type system that supports as many Elixir idioms as possible Balancing simplicity and pragmatism in type system design Addressing challenges like typing maps, pattern matching, and guards The tradeoffs between Dialyzer and making types part of the core language Advantages of typing for catching bugs, documentation, and tooling The differences between typing in the Gleam programming language vs. Elixir The possibility of type inference in a set-theoretic type system The history and development of set-theoretic types over 20 years Gradual typing techniques for integrating typed and untyped code How José and Giuseppe initially connected through research papers Using types as a form of "mechanized documentation" The risks and tradeoffs of choosing syntax Cheers to another decade of Elixir! A big thanks to this season's guests and all the listeners! Links and Resources Mentioned in this Episode: Bringing Types to Elixir | Guillaume Duboc & Giuseppe Castagna | ElixirConf EU 2023 (https://youtu.be/gJJH7a2J9O8) Keynote: Celebrating the 10 Years of Elixir | José Valim | ElixirConf EU 2022 (https://youtu.be/Jf5Hsa1KOc8) OCaml industrial-strength functional programming https://ocaml.org/ ℂDuce: a language for transformation of XML documents http://www.cduce.org/ Ballerina coding language https://ballerina.io/ Luau coding language https://luau-lang.org/ Gleam type language https://gleam.run/ "The Design Principles of the Elixir Type System" (https://www.irif.fr/_media/users/gduboc/elixir-types.pdf) by G. Castagna, G. Duboc, and J. Valim "A Gradual Type System for Elixir" (https://dlnext.acm.org/doi/abs/10.1145/3427081.3427084) by M. Cassola, A. Talagorria, A. Pardo, and M. Viera "Programming with union, intersection, and negation types" (https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf), by Giuseppe Castagna "Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)" (https://www.irif.fr/~gc/papers/covcon-again.pdf) by Giuseppe Castagna "A reckless introduction to Hindley-Milner type inference" (https://www.lesswrong.com/posts/vTS8K4NBSi9iyCrPo/a-reckless-introduction-to-hindley-milner-type-inference) Special Guests: Giuseppe Castagna, Guillaume Duboc, and José Valim.

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 type), and how proofs of equalities can be used to cast terms from one type to another.Also, in exciting news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes.  I will be monitoring the group.  I believe you have to request to join, and then I approve (it might take me until later in the day to do that, just fyi).  The invitation link is here.  

In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier work of McBride, Swierstra, and Altenkirch (which I will cover in a later episode) on a new approach to making a type theory extensional.  The idea is to have equality types reduce, within the theory, to statements of extensional equality for the type of the values being equated.

In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection.  This rule says that propositional equality implies definitional equality.  Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal.  This immediately gives us undecidability of type checking for the theory, at least as usually realized.

In this episode of the Personality Hacker podcast, Joel and Antonia discuss the limits of understanding personality type theory without focusing on personal growth.   https://personalityhacker.com  

Do genetics play a role in determining your physique, and if so, how much? In this episode I am talking all about body type theory (a controversial topic that has been around since the 1940s). Learn about the origins of the ectomorph, mesomorph, endomorph theory and how to apply it to your nutrition + exercise plan!Other episodes to check out: 7 Ways to Increase Your Hydration For Weight Loss, Better Brain Function + MoreForget Keto + Paleo: THIS Is the Diet Trick You Need This New YearIf you get value from this episode, I would be overjoyed to have you share it with another female millennial or screenshot it and share on instagram, tagging me at @fitfeedbyreed.For more information on my coaching services and for tons of healthy recipes check out www.fitfeedbyreed.com

In this episode Joel and Antonia respond to a listener's question about navigating the fine line between type and real human behavior.   https://personalityhacker.com   

Medicine involves more than science and evidence-based experiments. In today's health climate—where there seems to be a conflict of interest between health care, on the one hand, and pharmaceutical companies and the privatization of medicine, the other hand—it is easy to overlook a more holistic approach that understands how illness is causally linked to both the mind and body. David Corfield (University of Kent, UK) is Associate Professor of Philosophy, with special interests in the philosophies of mathematics, science, logic, medicine, history, and psychoanalysis. He discusses the importance of the role of the mind in medicine, and more generally, how a well-rounded approach to academic research and investigation provides a much more balanced and informed perspective.Living Philosophy is brought to you by Philosophy2u.com.Host:Dr Todd MeiSponsors:Philosophy2u.comHillary Hutchinson, Career and Change Coach at Transitioning Your LifeHermeneutics in Real LifeGeoffrey Moore, author of The Infinite Staircase     Links Related to this Episode:David Corfield (Wikipedia | University of Kent)Twitter (@DavidCorfield8)Why Do People Get Ill? by Corfield and Leader (Amazon)Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy (Oxford University Press)Darian Leader (Psychoanalyst)Thomas Kuhn (SEP)Imre Lakatos (SEP)Alasdair MacIntyre (Wikipedia)Albert Lautman (Wikipedia)R. G. Collingwood (SEP)John Ruskin (Wikipedia)Lacanian Psycholanalysis (Wikipedia)Vienna Circle (SEP)Type Theory (SEP)Idiographic vs. Nomothetic Analysis (Wikipedia)Music: Earth and the Moon, by KetsaLogo Art: Angela Silva, Dattura Studios

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.

Moobarkfluff! Taebyn is very excited about a new branch of math-Homotopy Type Theory. Give our weekly challenge a try this week and tell us about it on the BFFT chat. Lots of discussion on Last Week Today.  Who remembers Cop Rock? Taebyn issues so many challenges this week. Can you do them all? We visit the Trasfurmation Station. How is time reckoned in Star Trek? Frog is starting to sound like a certain mouse. Will Tater accept the commission to draw a wallaby wearing a sock? Only time will tell, and time is what is in rare supply during this episode, so spend some time with us, you will laugh, you will cry (let's face it, you will probably cry more out of pity), you will sigh and high five!   Moobarkfluff! https://www.bonfire.com/store/bearly-furcasting/Support the show (https://ko-fi.com/bearlyfurcasting)

Photo taken by Alasdair in the Caucasus mountains in Georgia (the country). Listen and explore:A brief summary of extraversion and introversionYou are not an ambivertThe extravert bias in our Western culture and what this means for introvertsHiding in the restroom as an introvert during a business conferenceSelf-awareness and approaching situations based on your personality preferencesWhat is a restorative niche? Why can  we all benefit from them?Alasdair's and Julie-Roxane's restorative niches at work and homeSelf-care means being a friend to yourselfJulie-Roxane flashes Alasdair on the podcastMentioned on this episode:Quiet: The Power of Introverts in a World That Can't Stop Talking by Susan CainWild Within book clubRebecca SolnitBill PlotkinConnect with us:Website: www.thefarout.lifeEmail us at info@thefarout.lifeAlasdair @ www.alasdairplambeck.comSupport this podcast:Discount link to purchase organic, raw ceremonial-grade cacao locally sourced in Guatemala (a portion of proceeds support this podcast)Become a patron at: https://www.patreon.com/thefaroutcoupleMake one-time donation with PayPal (our account is aplambeck22@gmail.com)Leave a review on iTunes!Share this episode with a friend! :DCredits:Intro music: "Complicate ya" by Otis McDonaldOutro music: "Running with wise fools" written & performed by Krackatoa (www.krackatoa.com)

Brian breaks down Robert Ringer’s “Three Types of people you’ll meet in the business world,” from his classic book, Winning Through Intimidation. Transcription Robert Ringer’s three type theory. Hi I’m Brian Pombo, welcome back to Brian J. Pombo Live. One of my favorite business books out there, Winning Through Intimidation. And it’s not a book […] The post Robert Ringer's Three Type Theory

Brian breaks down Robert Ringer's "Three Types of people you'll meet in the business world," from his classic book, Winning Through Intimidation. https://www.youtube.com/watch?v=C4pWvtYlEMw Transcription Robert Ringer's three type theory. Hi I'm Brian Pombo, welcome back to Brian J. Pombo Live. One of my favorite business books out there, Winning Through Intimidation. And it's not a book about how to intimidate people, but how to get around kind of the rules of intimidation, so to speak, that are already exist within human interaction. And great book, it came out in the 70s. It's still a fabulous book today. Robert Ringer is still with us, and he continues to produce articles on regular basis on his website. I believe it's RobertRinger.com. And I want to talk a little bit about his three types theory because it's interesting. But first, I wanted to remind you about my own book, 9 Ways to Amazon-Proof Your Business. If you haven't read it yet, go get yourself a free copy at AmazonProofBook.com. Grab it while you still can free copy AmazonProofBook.com. So let's talk about Robert Ringer, shall we it this is from let's see, this is from chapter four. He calls it the my three unforgettable professors at Screw U. And his three type theory comes down to there's there are only three types of people in business world with the one exception noted above. Okay, the one exception noted above, he's he's talking about. I'll get to that in a second. Let me talk about the three that he mentions here though, type number one, okay. This is the type of person so no matter what type of interaction you're getting with people, these are the type of people you deal with. Number One: "Who let you know that from the outset, either through his words, his actions, or both, that he's out to get your chips. He then follows through by attempting to do just that." That's type number one. Type number Two: "Who goes to great lengths to assure you that he would never dream of pilfering your chips, often trying to throw you off guard by assuring you that he really wants to see you get everything that's coming to you. Then like type number one, and without hesitation, he goes about trying to grab your chips anyways. " Here's Type number Three: "Who like type number two assures you that he's not interested in your chips. Unlike type number two, however, he sincerely means what he says. But that's where the difference ends. Due to any one of a number of reasons ranging from his own bungling, to his amoral standards for rationalizing what's right and wrong. He, like type number one, and two, still ends up trying to grab your chips. Which means that his suppose that good intentions are irrelevant to the final outcome. In summation, no matter how someone posits himself, you would be wise to assume that he will, in the final analysis, attempt to grab your chips." So what's this have to do with anything, right? It has to do with the basic concept that people are people. And no matter how a person holds themselves, in the end, everybody tends to look out for themselves in the end, or their families, they tend to look out for their own interest. And it's a very natural thing. It's not anything to be scared about, or to think that a person's naturally immoral just because they're out for themselves. That's just, it's a survival mechanism. If nothing else, people have to be able to look out for themselves. I deal a lot with the self reliance field. I run the podcast called, the Off The Grid Biz Podcast. Which is all about the self reliance industry, meaning people and products that are encouraging people to become more self reliant in some way. Okay. And the interesting thing is, it's built into that concept of self reliance that people have an interest in being self reliant to begin with, that it's just a natural thing one way or the other. Yeah, in the short run,

Carlo is a postdoc in the Computer Science Department at Carnegie Mellon University, where he received a Ph.D. under Robert Harper. He previously studied at Indiana University Bloomington, where he received a B.S. in Mathematics and in Computer Science. Today Carlo joined us to discuss Homotopy Type Theory, a new foundations for mathematics based on a recently-discovered connection between Homotopy Theory and Type Theory. Carlo explains intuitively what Homotopy Type Theory is and how it is used, and then goes over various possible implementations of Homotopy Type Theory in a theorem-proving environment such as Coq. Finally, he fields questions on Homotopy Type Theory, theorem-proving, and other topics from the Boston Computation Club audience. The Boston Computation Club can be found at https://bstn.cc/ Carlo Angiuli can be found at https://www.cs.cmu.edu/~cangiuli/ A video recording of this talk is available at https://youtu.be/VMqF06fDljU For more on Homotopy Type Theory refer to https://homotopytypetheory.org/book/

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 (Identity Extension), the Identity Inclusion lemma identifies certain types whose relational meaning is included in the identity relation, and certain types which include the identity relation. So there are two subset relations, going in opposite directions. The two classes of types are first, the ones where all quantifiers occur only positively, and second, where they occur only negatively. Using Identity Inclusion, we can derive transitivity for forall-positive types, which is needed to derive induction following the natural generalization of the scheme in Wadler's paper (last episode).

Welcome to the Christmas special community edition of MLST! We discuss some recent and interesting papers from Pedro Domingos (are NNs kernel machines?), Deepmind (can NNs out-reason symbolic machines?), Anna Rodgers - When BERT Plays The Lottery, All Tickets Are Winning, Prof. Mark Bishop (even causal methods won't deliver understanding), We also cover our favourite bits from the recent Montreal AI event run by Prof. Gary Marcus (including Rich Sutton, Danny Kahneman and Christof Koch). We respond to a reader mail on Capsule networks. Then we do a deep dive into Type Theory and Lambda Calculus with community member Alex Mattick. In the final hour we discuss inductive priors and label information density with another one of our discord community members. Panel: Dr. Tim Scarfe, Yannic Kilcher, Alex Stenlake, Dr. Keith Duggar Enjoy the show and don't forget to subscribe! 00:00:00 Welcome to Christmas Special! 00:00:44 SoTa meme 00:01:30 Happy Christmas! 00:03:11 Paper -- DeepMind - Outperforming neuro-symbolic models with NNs (Ding et al) 00:08:57 What does it mean to understand? 00:17:37 Paper - Prof. Mark Bishop Artificial Intelligence is stupid and causal reasoning wont fix it 00:25:39 Paper -- Pedro Domingos - Every Model Learned by Gradient Descent Is Approximately a Kernel Machine 00:31:07 Paper - Bengio - Inductive Biases for Deep Learning of Higher-Level Cognition 00:32:54 Anna Rodgers - When BERT Plays The Lottery, All Tickets Are Winning 00:37:16 Montreal AI event - Gary Marcus on reasoning 00:40:37 Montreal AI event -- Rich Sutton on universal theory of AI 00:49:45 Montreal AI event -- Danny Kahneman, System 1 vs 2 and Generative Models ala free energy principle 01:02:57 Montreal AI event -- Christof Koch - Neuroscience is hard 01:10:55 Markus Carr -- reader letter on capsule networks 01:13:21 Alex response to Marcus Carr 01:22:06 Type theory segment -- with Alex Mattick from Discord 01:24:45 Type theory segment -- What is Type Theory 01:28:12 Type theory segment -- Difference between functional and OOP languages 01:29:03 Type theory segment -- Lambda calculus 01:30:46 Type theory segment -- Closures 01:35:05 Type theory segment -- Term rewriting (confluency and termination) 01:42:02 MType theory segment -- eta term rewritig system - Lambda Calculus 01:54:44 Type theory segment -- Types / semantics 02:06:26 Type theory segment -- Calculus of constructions 02:09:27 Type theory segment -- Homotopy type theory 02:11:02 Type theory segment -- Deep learning link 02:17:27 Jan from Discord segment -- Chrome MRU skit 02:18:56 Jan from Discord segment -- Inductive priors (with XMaster96/Jan from Discord) 02:37:59 Jan from Discord segment -- Label information density (with XMaster96/Jan from Discord) 02:55:13 Outro

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 forget to follow Ben on twitter @GhostofBendy

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 forget to follow Ben on twitter @GhostofBendy

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 forget to follow Ben on twitter @GhostofBendy

I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.

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.

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 graphs as the relational meaning.

Equal parts science and art, programming language design is very much an unsolved problem. This week, Ron speaks with Leo White, from Jane Street's Tools & Compilers team, about cutting-edge language features, future work happening on OCaml, and Jane Street's relationship with the broader open-source community. The conversation covers everything from the paradox of language popularity, to advanced type system features like modular implicits and dependent types. Listen in, no programming languages PhD required!

Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics) for conversion checking. This is the process of confirming that types are equivalent during type checking, which, due to dependent types, can require checking program equivalence. The latter is usually restricted to just beta-equivalence (where beta-reduction is substitution of argument for input variable when applying a function), because richer notions of program equivalence are usually undecidable. I have a mini-rant in this episode explaining why this usual requirement of normalization for conversion checking is not sensible.Also I note that you can find the episodes of the podcast organized by chapter on my web page.

We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress. Discussion of progress in the context of type theory, where adding axioms can lead to a failure of progress.

In this episode, Jesse and JP dive in to opaque result types, which could help prevent leaking of implementation details to library consumers.

The Never type has some very unique properties and behavior. We introduce the type and discuss a recent proposal (SE-215) to make it conform to Hashable and Equatable.

Types in programming languages are commonly thought of as a way of preventing certain bad things from happening, such as multiplying a number by a string. But this is only half of the benefit of types: it is what types are against. Types in programming languages are also what enable some good things to happen, such as selecting the right implementation of a heterogeneous operation like comparison or printing based on type information; this is what are types for. This ability is surprisingly powerful, and gives rise to a variety of highly expressive generic programming techniques. Jeremy illustrates with some examples based on the rank-polymorphic array operations introduced in Iverson’s APL: not only does the type information prevent array shape errors, it is what directs the lifting of operations across array dimensions.

In this presentation, Uday brings together two strands of Christopher Strachey’s thought: parametric polymorphism and abstract models of storage. The term parametric polymorphism was introduced in by Strachey who distinguished it from “ad hoc” polymorphism. In the words of John Reynolds, “a parametric polymorphic function is one that behaves the same way for all types,” whereas an ad hoc polymorphic function may have unrelated meanings at different types. A very similar intuition arose in mathematics, some twenty years earlier, for which Eilenberg and MacLane proposed a “General Theory of Natural Equivalences”, what we now call category theory. Relating the two notions allows us to develop a broad view of “parametricity” (the idea of acting the same way for all types), which is applicable not only to programming languages but also to mathematics and perhaps other disciplines. A particularly important application of this broad view is for Strachey’s “mathematical semantics” of programming languages. For modelling imperative programming languages that operate by manipulating a store, Strachey presented a basic model of storage based on “locations”, while promising a further paper on an “abstract model of storage” to appear in future. Unfortunately the latter never appeared. In succeeding work, Reynolds proposed an abstract model of store as well as an “intuitionistic” functor category approach to model the stack discipline of the store. O'Hearn and Tennent made the crucial observation that the model needs to be embellished with parametricity to capture the data abstraction aspects of the store. In this talk, Uday reviews these developments as well as his own recent work on integrating the Reynolds model with parametricity to capture the fact that state changes of the store are irreversible. One way to understand these developments is to view them as a “parametric mathematical semantics” of programming languages.

Your favorite features of Type Systems in one episode! Interfaces, Generics, ADT, Type Classes and Dependent Types. We'll talk about what they are and how they shape the way we work. Code Podcast Forum: https://discuss.codepodcast.com/t/episode-5-type-systems/22 Episode produced by: Andrey Salomatin https://twitter.com/flpvsk Michael Beschastnov michael@codepodcast.com Guests (in order of appearance): Joseph Abrahamson https://twitter.com/sdbo Radoslav Kirov https://twitter.com/radokirov Erlend Hamberg https://twitter.com/ehamberg Edwin Brady https://twitter.com/edwinbrady Special thanks to our reviewers, this time: Adriano Melo https://twitter.com/AdrianoMelo Roman Liutikov https://twitter.com/roman01la If you'd like to help us make the podcast better *and* get episodes earlier, consider becoming a reviewer: https://gist.github.com/filipovskii/f12685bc74a425ba651c736fb5e3e5ae ## Links: Basics Benjamin C. Pierce "Types and Programming Languages" https://www.cis.upenn.edu/~bcpierce/tapl/ A draft of the book available for free: http://ropas.snu.ac.kr/~kwang/520/pierce_book.pdf Rob Nederpelt and Herman Geuvers "Type Theory and formal proof" http://www.win.tue.nl/~wsinrpn/book_type_theory.htm Robert Harper "Practical Foundations for Programming Languages" https://www.cs.cmu.edu/~rwh/pfpl.html Interview with Jesper Louis Andersen about Erlang, Haskell, OCaml, Go, Idris, the JVM, software and protocol design — PART I https://notamonadtutorial.com/interview-with-jesper-louis-andersen-about-erlang-haskell-ocaml-go-idris-the-jvm-software-and-b0de06440fbd#.rawqi9bvp Paper by Xavier Leroy "Manifest Types, Modules, and Separate Compilation" (1994) http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.3950 Paper by Conor McBride and Ross Paterson "FUNCTIONAL PEARL: Applicative programming with effects" http://strictlypositive.org/IdiomLite.pdf ## Links: Idris Edwin Brady "Type-Driven Development with Idris" http://tinyurl.com/typedd ## Links: TypeScript http://www.typescriptlang.org/ ## Links: Haskell Christopher Allen and Julie Moronuki "Haskell Programming from First Principles" http://haskellbook.com/ Learn you some Haskell http://learnyouahaskell.com/ ## Links: Scala Paul Chiusano and Rúnar Bjarnason "Functional Programming in Scala" https://www.manning.com/books/functional-programming-in-scala ##Links: OCaml Yaron Minsky, Anil Madhavapeddy, Jason Hickey "Real World Ocaml" https://realworldocaml.org A chapter from "Real World Ocaml" about Objects https://realworldocaml.org/v1/en/html/objects.html OCaml Documentation http://caml.inria.fr/pub/docs/manual-ocaml/ Effective ML (video) https://blogs.janestreet.com/effective-ml-video/ ## Links: Discussions What exactly makes the Haskell type system so revered (vs say, Java)? http://softwareengineering.stackexchange.com/questions/279316/what-exactly-makes-the-haskell-type-system-so-revered-vs-say-java What is a Functor? http://stackoverflow.com/questions/2030863/in-functional-programming-what-is-a-functor#2031421 ADTs vs Inheritance http://stackoverflow.com/questions/3271974/why-adts-are-good-and-inheritance-is-bad Existential vs Universal Typess http://stackoverflow.com/questions/14299638/existential-vs-universally-quantified-types-in-haskell#14299983 Subclassing vs Subtyping http://www.cs.princeton.edu/courses/archive/fall98/cs441/mainus/node12.html Why Haskell has no subtyping https://www.reddit.com/r/haskell/comments/423o0c/why_no_subtypingsubtype_polymorphism/ Haskell vs Java type systems http://softwareengineering.stackexchange.com/questions/279316/what-exactly-makes-the-haskell-type-system-so-revered-vs-say-java ## Music Mid-Air! @mid_air

PHQ | QUESTIONS FROM COMMUNITY: In this episode Joel and Antonia answer a question about music type theory and the idea of having a donation button on the Personality Hacker website. http://www.PersonalityHacker.com

Episode 3: Dan Licata on Homotopy Type Theory

Erich Reck (UC Riverside) gives a talk at the MCMP workshop "Carnap on Logic" (3-6 July, 2013) titled "Logic in the 1930s: Type Theory and Model Theory".

Steve Awodey (CMU/MCMP) gives a talk at the MCMP Colloquium (13 June, 2012) titled "Homotopy Type Theory and Univalent Foundations of Mathematics". Abstract: Recent advances in foundations of mathematics have led to some developments that are significant for the philosophy of mathematics, particularly structuralism. The discovery of an interpretation of constructive type theory into homotopy theory suggests a new approach to the foundations of mathematics with both intrinsic geometric content and a computational implementation. In this setting, leading homotopy theorist Vladimir Voevodsky has proposed new axiom for foundations with both geometric and logical significance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice, according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to homotopy type theory, and forms the basis of the new Univalent Foundations Program.