TopPodcast.com
Menu
  • Home
  • Top Charts
  • Top Networks
  • Top Apps
  • Top Independents
  • Top Podfluencers
  • Top Picks
    • Top Business Podcasts
    • Top True Crime Podcasts
    • Top Finance Podcasts
    • Top Comedy Podcasts
    • Top Music Podcasts
    • Top Womens Podcasts
    • Top Kids Podcasts
    • Top Sports Podcasts
    • Top News Podcasts
    • Top Tech Podcasts
    • Top Crypto Podcasts
    • Top Entrepreneurial Podcasts
    • Top Fantasy Sports Podcasts
    • Top Political Podcasts
    • Top Science Podcasts
    • Top Self Help Podcasts
    • Top Sports Betting Podcasts
    • Top Stocks Podcasts
  • Podcast News
  • About Us
  • Podcast Advertising
  • Contact
Not in our directory?
Add Show Here
Podcast Equipment
Center

toppodcastlogoOur TOPPODCAST Picks

  • Comedy
  • Crypto
  • Sports
  • News
  • Politics
  • True Crime
  • Business
  • Finance

Follow Us

toppodcastlogoStay Connected

    View Top 200 Chart
    Back to Rankings Page
    Technology

    Type Theory Forall

    An accessible podcast about Type Theory, Programming Languages Research and related topics.

    Advertise

    Copyright: © CC BY 4.0

    • Apple Podcasts
    • Google Play
    • Spotify

    Latest Episodes:
    #33 Z3 and Lean, the Spiritual Journey - Leo de Moura Sep 09, 2023

    Not satisfied with implementing one of the most popular automated theorem provers, Z3, Leo de Moura also tackles another extremely hard problem in our field and implements a brand new interactive theorem prover from scratch, Lean. In this episode we dive into the mind and philosophy of this man.

    Links

    • Leo’s Website
    • Lean
    • Z3
    • The Church of Logic Podcast

    #32 TyDe Systems - Jan de Muijnck-Hughes Jul 22, 2023

    In this episode we continue our conversation with Jan de Muijnck-Hughes a Research Associate at Glasgow University. He works using all sorts of fancy type systems mostly targeted for hardware specification, particularly with the aid of the theorem prover Idris. This episode we start by talking a little about Impostor Syndrome in academia and how he has learned to cope with it and then we dive deeper into the technicalities of his research, in particular his philosophy on Type Directed Design of Systems. We talk about Session Types, Graded Types, Quantitative types, etc.

    Don’t forget to join our new discord channel!

    If you like our show please consider donating any amount at ko-fi.

    Links

    • Jan’s website
    • Jan’s twitter
    • Jan’s mastodon
    • Writing and Speaking with Style
    • Artifact Eval
    • Andrej Bauer: Formalising Invisible Mathematics
    • Hedy language (Felienne Hermans)
    • Hermans’ Inaugural Lecture on making PL human and inclusive
    • Epistemic Injustice
    • Richard Eisenberg interview
    • ‘Software Foundations’ but in Agda
    • ‘System F for Fun & Profit’
    • Reviewing

    Project Pages

    • https://dsbd-appcontrol.github.io/
    • https://border-patrol.github.io/

    Cool People

    • Rachit Nigam
    • Clement Pit-Claudel

    Software

    • Idris Language
    • Biblio

    #31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes Jul 13, 2023

    In this episode we have a deep conversation with Jan de Muijnck-Hughes, talks about all the cool research he has done with idris, hardware and different kinds of interesting type systems such as session types, quantitative types and graded types. In the second half we discuss all the different kinds of problems that has been going on in PL academia lately and what we can do as a community to address those issues.

    Also, we have a discord channel now, join us!

    If you like our show please consider donating any amount at ko-fi.

    Errata:

    • Jan mentions ‘Jeff Foster’ when, in fact, he meant Nate Foster
    • This is the SIGCOMM ‘Call’: https://sigcomm.quest/
    • Felinne Hermans did her PhD at Eindhoven and not Delft

    Links

    • Jan’s website
    • Jan’s twitter
    • Jan’s mastodon
    • Writing and Speaking with Style
    • Artifact Eval
    • Andrej Bauer: Formalising Invisible Mathematics
    • Hedy language (Felienne Hermans)
    • Hermans’ Inaugural Lecture on making PL human and inclusive
    • Epistemic Injustice
    • Richard Eisenberg interview
    • ‘Software Foundations’ but in Agda
    • ‘System F for Fun & Profit’
    • Reviewing

    Project Pages

    • https://dsbd-appcontrol.github.io/
    • https://border-patrol.github.io/

    Cool People

    • Rachit Nigam
    • Clement Pit-Claudel

    Software

    • Idris Language
    • Biblio

    #30 Actors, GADTs and Burnout - Dan and Pedro May 30, 2023

    In this episode we have over Dan Plyukhin, a PhD Candidate from the University of Illinois Urbana-Champaign.

    We talk about Dan’s research is in the field of parallelism, more specifically garbage collection in the presence of actors.

    Then we also talk about Pedro’s research on translating GADTs from OCaml to Coq, and the burnout process that lead him to take 10 months off from his PhD to be with his family back in Brazil.

    Links

    • Dan’s Personal Website
    • Twitter: @dplyukhn

    #29 Can PL theory make you a better software engineer? - Jimmy Koppel Apr 09, 2023

    Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where he teaches engineers to write better code! In this interview we talk about how to make better code, how the knowledge of computer science theory and programming languages can help engineers to achieve that, and much more!

    Links

    • Jimmy’s Personal Website
    • Jimmy’s Twitter
    • Mirdin’s Website
    • Jimmy’s Blog
    • Lastest blog post
    • One CFG-Generator to Rule Them All
    • Automatically Deriving Control-Flow Graph Generators from Operational Semantics
    • Thiel Fellowship

    Newsletters discussed in the show

    • Mirdin’s Newsletter
    • Hillel Wayne’s Newsletter
    • Eric Normand’s Newsletter
    • Jeremy Kun’s Newsletter

    #28 Formally Verifying Smart Contracts - Pruvendo Feb 15, 2023

    In this episode we host another company that does formal method in the context of the Everscale Blockchain, and Solidity smart contracts. How and why they use formal methods in this context? Who are their clients? What are the caveats?

    Links

    • Pruvendo’s Website
    • Pruvendo’s Linkdin
    • Pruvendo’s Twitter

    #27 Formalizing an OS: The seL4 - Gerwin Klein Feb 04, 2023

    In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine.

    Links

    • Gerwin’s Twitter
    • Gerwin’s Website
    • ProofCraft’s Website

    #26 Mechanizing Modern Mathematics - Kevin Buzzard Jan 16, 2023

    Kevin Buzzard has been very passionate spreading the word among mathematicians to use theorem provers mechanize theorems of modern mathematics. In this conversation we will talk about his vision in teaching undergrads to use the Lean theorem prover, what is the Xena Project, his view of how theorem provers can change the way we do mathematics, and much more!

    Links

    • Xena’s Project Twitter
    • Xena Project’s Website
    • Lean’s Website

    #25 Formally Verifying the Tezos Codebase - Formal Land Nov 21, 2022

    In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the past developing new features to their source-to-source compiler CoqOfOcaml. In this episode we talk about their work with Tezos and how their techniques are applicable to other codebases as well! For this we talk with Formal Land founder Guillaume Claret and the proof engineers Daniel Hilst and Pierre Vial.

    Links

    • Formal Land Website
    • Formal Land Email: contact@formal.land
    • Formal Land Twitter: @LandFooBar
    • CoqOfOcaml
    • The DAO hack

    #24 The History of Isabelle - Lawrence Paulson Oct 06, 2022

    In this episode we interview Lawrence Paulson, one of the creating fathers of Isabelle.

    We talk about the development process, how it drew inspirations and ideas from LCF and Boyer Moore. What tools were used, it’s strenghts and weaknesses, and all about the historical context at the time! We also briefly talk about his formalization of the Gödel’s Incompletenes theorems in Isabelle

    Paulson have quite an extensive CV, he is a professor at Cambridge, have published more than 100 papers, is an ACM fellow since 2008, is a member of the royal society since 2017, among many other things!

    Links

    • Larry’s Website
    • Larry’s Twitter
    • Larry’s Blog

    #23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich Sep 24, 2022

    In this episode we talk about Sigplan, the organization behind the most important conferences and proceedings in our field. What is the SIGPLAN? What exactly does it do? How is it organized? How are things published? To answer these and many other questions we talk with Jens Palsberg, a professor at UCLA, who is the past chair of the SIGPLAN. And also Jonathan Aldrich, a professor at the CMU, who is a member of the ACM publication board.

    Links

    • Jen’s Website
    • Jonathan’s Website
    • Jonathan’s Twitter
    • Sigplan Blog
    • Post on Hybrid Conferences
    • SIGPlAN-M Mentoring Program

    #22 Impredicativity, LEM, Realizability and more - Cody Roux Aug 12, 2022

    In this episode Cody Roux teaches some interesting concepts that people care about in Mathematics and Logic as a way to try to understand what is going on in the universe around us! In particular we will try to explain concepts such as Impredicativity, Excluded Middle, Group Theory, Model Theory, Kripke Models, Realizability, The Markov Principle, Cut Elimination, and other stuff!

    Links

    • Cody’s website
    • Cody’s dblp

    #21 Denotational Design - Conal Elliott Aug 04, 2022

    In this episode Conal Elliott gives a more concrete presentation on 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 philosophical conversation to explain why he believes that Denotational Design is a superior form of reasoning in the realm of computer science.

    We also continue a discussion raised by Dan Ghica on the last episode on the need for Operational Semantics and the role of elegance in reasoning and design.

    Along the way we also address the questions sent by the listeners in these last episodes.

    Links

    • Conal’s website
    • Play/work with Conal
    • Conal’s twitter: @conal
    • The simple essence of automatic differentiation
    • Compiling to categories
    • Generic parallel functional programming
    • Denotational design with type class morphisms

    Quotes

    • “A theory appears beautiful or elegant […] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons.” - Murray Gell-Mann, Beauty and Elegance in Physics.

    • “In Galileo’s time, professors of philosophy and theology—the subjects were inseparable—produced grand discourses on the nature of reality, the structure of the universe, and the way the world works, all based on sophisticated metaphysical arguments. Meanwhile, Galileo measured how fast balls roll down inclined planes. How mundane! But the learned discourses, while grand, were vague. Galileo’s investigations were clear and precise. The old metaphysics never progressed, while Galileo’s work bore abundant, and at length spectacular, fruit. Galileo too cared about the big questions, but he realized that getting genuine answers requires patience and humility before the facts.” - Frank Wilczek, (The Lightness of Being: Mass, Ether, and the Unification of Forces)

    • “We must make here a clear distinction between belief and faith, because, in general practice, belief has come to mean a state of mind which is almost the opposite of faith. Belief, as I use the word here, is the insistence that the truth is what one would ‘lief’ or wish it to be. The believer will open his mind to the truth on the condition that it fits in with his preconceived ideas and wishes. Faith, on the other hand, is an unreserved opening of the mind to the truth, whatever it may turn out to be. Faith has no preconceptions; it is a plunge into the unknown. Belief clings, but faith lets go. In this sense of the word, faith is the essential virtue of science, and likewise of any religion that is not self-deception.” - Alan Watts (The Wisdom of Insecurity: A Message for an Age of Anxiety)


    #20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica Jun 27, 2022

    In this episode, me and Eric Bond have a great conversation with Dan R. Ghica, a professor at Birmingham University and Director of the Programming Language Research Lab of the Huaweii Research Centre Edinburgh. We talk about his work on both institutions, which includes topics such as Category Theory, String Diagrams, and Game Semantics. We also briefly discuss the current publication process of our field and entertain some thoughts on how to make it better. Finally, we touch on more personal topics such as his views about Elegance, making an insightful counterpoint to Conal’s opinions on Denotational Semantics vs. Operational Semantics.

    Links

    • Dan’s Twitter: @danghica
    • Dan’s Website
    • Job advert for Huawei positions

    Talks and Lectures

    • Dan’s talk on Syntactic Trinitarianism (terms, graphs, diagrams)
    • Dan’s talk on a similar, more semantics-oriented talk at TERMGRAPH
    • Dan’s OPLSS course on (denotational) game semantics
    • Game semantics lectures

    Papers

    • Paper on string diagrams and their applications to reverse automatic differentiation (long paper, part of it to appear in FSCD 2020)
    • Paper on automatic differentiation and string diagrams
    • Paper on effect handlers
    • Paper on optimisation with constructive reals
    • Paper on digital circuits and string diagrams
    • Paper on functorial boxes for string diagrams
    • A Game semantics paper mentioned during the conversation
    • Decidability via game semantics
    • Landmark paper on undecidability of observational equivalence

    Other Links

    • Penrose book
    • Book on type-level string diagrams
    • Proof assistant for higher categories
    • The Programming Journal
    • Midlands Graduate School

    #19 Experience Report: Learning Coq - Patrick and Supun Jun 04, 2022

    In today’s episode I invite two friends of mine Patrick Lafontaine and Supun Abeysinghe. We will talk about their experience learning Coq and we guide ourselves 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 with Rust. And Supun works more along the lines of machine learning in the context of systems.


    #18 Gödel's Incompleteness Theorems - Cody Roux May 19, 2022

    In this episode Cody Roux talks about the Gödel’s Incompleteness Theorems. We go through it’s underlying historical context, Hilbert’s Program, how it relates with 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’s Theorems
    • Jeremy Avigad’s Lecture Notes

    #17 The Lost Elegance of Computation - Conal Elliott May 09, 2022

    In this episode I had the pleasure to have an in-depth conversation with Conal Elliott about his life, his work, his philosophy and his many opinions about research and the current state of PL Research and how it lead him to come with the concept of Denotational Design. Conal got his PhD at CMU in the 90s under Frank Pfenning working on Higher-Order Unification, after that he has devoted his life on thinking and refining graphic computation and the tools behind it.

    Links

    • Conal’s website
    • Play/work with Conal
    • Conal’s twitter: @conal
    • The simple essence of automatic differentiation
    • Compiling to categories
    • Generic parallel functional programming
    • Denotational design with type class morphisms
    • Functional Images
    • Functional Reactive Animation
    • Alphabet Versus the Goddess - Leonard Shlain
    • The information - James Gleick
    • Murray Gell-Mann’s definition of beauty/elegance: “A theory appears beautiful or elegant […] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons.”
    • A John Backus quote (from his Turing Award lecture): “Many creative computer scientists have retreated from inventing languages to inventing tools for describing them. Unfortunately, they have been largely content to apply their elegant new tools to studying the warts and moles of existing languages. After examining the appalling type structure of conventional languages, using the elegant tools developed by Dana Scott, it is surprising that so many of us remain passively content with that structure instead of energetically searching for new ones.”

    #16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx Apr 02, 2022

    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, the Uniqueness of Identity of Proofs, UIP for short, and why it is inconsistent with Homotopy Type Theory.

    Links

    • Jesper’s Website
    • Jesper’s Twitter: @agdakx
    • Jesper’s PhD Thesis
    • Rewrite Theory paper
    • Pattern matching without K paper (Check his website for more)
    • EuroProofNet
    • WITS Talks on Youtube (Workshop on the Implementation of Type Systems)
    • Agda Zulip
    • Agda Mailing List
    • Ataca Github
    • Wadler’s book on Agda
    • Stump’s book on Agda

    #15 Coq Projects, Agda, Idris, Kind - Nitin and Eric Mar 27, 2022

    In this episode me, Eric and Nitin continues our conversation started in the last episode. This time we move our attention to the cool projects happening in Coq, in particular commenting through the projects mentioned in Andrew Appel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” that took place in CPP’22 which is colocated with POPL and towards the end we also talk about agda, idris and Kind.

    Links

    • Nitin Twitter @NitinJohnRaj2
    • Eric Twitter @EricBond10
    • Appel’s CPP Talk
    • Proof Assistants Stack Exchange
    • Coq Community
    • Leo de Moura Interview

    #14 POPL, Parametricity, Scala, DOT - Nitin and Eric Feb 12, 2022

    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
    • Reynolds Paper
    • Practical Foundations for Programming Languages

    #13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley Dec 23, 2021

    This episode is about the journey of a programmer that converted himself into a 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 make him learn Coq and Category Theory?
    • How does Coq compare with ACL2?
    • How do both Coq and ACL2 compares to TLA+?
    • Did learning Coq make John a better programmer?

    Links

    • John’s Email: johnw@newartisans.com
    • John’s Twitter: @jwiegley

    #12 Tenure, Sexism and ADHD - Talia Ringer Nov 10, 2021

    Talia Ringer is an Assistant Professor at University of Illinois Urbana-Champaign. She did her PhD at University of Washington with her thesis on Proof Repair.

    She’s very active on twitter @taliaringer. And in this episode we will talk about her transition from PhD to Professor, her work on diversity, her ADHD and how it has affected her career so far, and we also touch on the delicate topic of sexism in academia.

    Links

    • Talia’s Twitter
    • Sigplan Mentoring
    • TIL: a type-directed, optimizing compiler for ML
    • Neuro Divergent in CS
    • Neuro Divergent in CS - Slack

    • Overblur

    #11 FP, Monads, GHC, and beyond - Alejandro Serrano Oct 04, 2021

    In this episode we have talk with Alejandro Serrano Mena, he works on 47 degrees and is a published author of two books about Haskell: The Book of Monads and Practical Haskell.

    We talk about many interesting features behind functional programming such as adts, pattern matching, impredicativity, monads, effects, hacking the ghc and how all this comes together to grab industry attention to adopt functional programming features over the past decade.

    Links

    • Our new twitter @ttforall
    • Alejandro’s twitter
    • Book of Monads
    • Practical Haskell
    • The Haskell Interlude
    • Tweag’s youtube channel on the GHC

    #10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das Jul 15, 2021

    In this episode we host a discussion between Anupam Das and Thorsten Altenkirch on the role of constructivism in mathematics, logic and computer science.

    Anupam is a lecturer in the University of Birmingham in the UK, and Thorsten Altenkirch is a CS Professor at the University of Nottingham.

    We discuss why constructive content in proofs matters, the law of excluded middle, the axiom of choice, category theory, and much more!

    Links

    • Thorsten’s website
    • Anupam’s website
    • Thorsten’s Book on Python
    • The Proof Theory Blog
    • High School Algebra
    • Stanford Encyclopedia of Philosophy

    #9 Logic and Proof Theory - Anupam Das May 28, 2021

    In this episode I interview Anupam Das we have a nice conversation on the historical perspective of how Logic and Proof Theory as we know today came about in the 30’s. The differences between Natural Deduction and Sequent Calculus, Cut Elimination and much more.

    Links

    • Anupam Das
    • The Proof Theory Blog
    • Stanford Encyclopedia of Philosophy
    • Anupam’s Talk on Cyclic Arithmetic

    #8 Cedille - Chris Jenkins May 10, 2021

    In this episode I have a nice conversation with Chris Jenkins to talk about the 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 the typing rules fit one page. And yet it is strong enough to do relevant theorem proving. This is probably the most technical episode so far.

    Links

    • Leroy Jenkins
    • Cedille Cast
    • The Iowa Type Theory Commute
    • Cedille Page
    • Github Page

    #7 Hacking Isabelle's Internals - Daniel Matichuk Apr 15, 2021

    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 of Aarch32 Arm Archtecture at Galois.


    #6 All The Dumb Questions on Gradual Types - Zeina Migeed Mar 29, 2021

    In this episode we interview Zeina Migeed, a PhD Student at University of California Los Angeles, advised by Prof. Jens Palsberg

    She Researches Gradual Types and had a paper published at POPL’20 named “What is Decidable about Gradual Types”. here is a link to it

    As the name of the episode suggests, I’ll be asking her all the dumb questions related to not only gradual types, but also intersection types and recursive types as well!


    #5 The History of Coq'Art - Yves Bertot Feb 27, 2021

    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 dans les documents structurés - Check figure 15 for an example on how Yves’ tools would build trees internally

    A video showing his tool in practice, doing proofs with mouse clicks

    A Genereic Approach to Building User Interfaces for Theorem Provers


    #4 Theorem Provers, Functional Programming and Companies - Eric Bond Feb 15, 2021

    In this episode we host Eric Bond to go through some real cool projects happening in the PL World and some of the companies behind them.

    We discuss some technical differences between the major interactive theorem provers out there, some of their most popular projects, and a few companies that work in the realm.

    Eric Bond works at 47 degrees, a consulting company on Functional Programming Languages, specially on Scala and Haskell. You can find Eric @ericbond10 on Twitter.

    During the episode we mention PL Talks and the Midlands Graduate School in the Foundations of Computing Science 2021.


    #3 ML for PL and Mental Health - Dan Zheng Feb 01, 2021

    In this episode we host Dan Zheng, an alumni of Purdue University that now works at Google at real cool projects that relates ML and PL.

    We chat about how was his transition from undergrad to such a huge company like 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 each other. And towards the end we shift our attention to mental health, both in the academia and in the industry.

    You can find Dan at twitter @dancherp


    #2 Grad School Life - Rajan Walia and John Sarracino Jan 10, 2021

    In this episode we host Rajan Walia and John Sarracino. Rajan is a last year PhD Student from Indiana University, working under Sam Tobin-Hochstadt. And John 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 more!

    Here you can find John’s Website. http://goto.ucsd.edu/~john/

    And here is Matt Might’s website mentioned in the episode. http://matt.might.net/#blog


    #1 What is PL research? - Prof. Ben Delaware Dec 23, 2020

    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


    #0 Cool Internships in PL - Believe or not there are quite a few companies interested in Programming Languages Research. Dec 14, 2020

    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 Shpat Morina. Click Here


      Related Podcasts

      The Steve Krebs Show

      1

      The Steve Krebs Show Society & Culture
      Artificial Intelligence News

      2

      Artificial Intelligence News News
      The Tripwire Cybersecurity Podcast

      3

      The Tripwire Cybersecurity Podcast Technology
      MacBreak Weekly (Audio) – TWiT

      4

      MacBreak Weekly (Audio) – TWiT News
      ServiceNow TechBytes

      5

      ServiceNow TechBytes Podcasting
      Shir ya Khat | شیریاخط

      6

      Shir ya Khat | شیریاخط Technology
      footer-logo

      Contact Us

      Toll Free: 844-670-7747

      Links

      • Home
      • Top Charts
      • Networks
      • Apps
      • Independents Podcasts
      • Podcast Advertising
      • Podcast News
      • Contact Us
      • About Us
      • Analytics & Insights

      Stay Connected

        Privacy, Terms of Use & Our Code of Ethics Protecting Content Creators Copyrights