• Iowa Type Theory Commute

  • Auteur(s): Aaron Stump
  • Podcast

Iowa Type Theory Commute

Auteur(s): Aaron Stump
Écouter gratuitement

  • Résumé

  • Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
    © 2025 Iowa Type Theory Commute
    Voir plus Voir moins
Mathématique Science
Voir plus Voir moins
Épisodes
  • Nominal Isabelle/HOL

    Nominal Isabelle/HOL
    Jan 31 2025

    In this episode, I discuss the paper Nominal Techniques in Isabelle/HOL, by Christian Urban. This paper shows how to reason with terms modulo alpha-equivalence, using ideas from nominal logic. The basic idea is that instead of renamings, one works with permutations of names.

    Voir plus Voir moins
    16 min
  • The Locally Nameless Representation

    The Locally Nameless Representation
    Jan 3 2025

    I discuss what is called the locally nameless representation of syntax with binders, following the first couple of sections of the very nicely written paper "The Locally Nameless Representation," by Charguéraud. I complain due to the statement in the paper that "the theory of λ-calculus identifies terms that are α-equivalent," which is simply not true if one is considering lambda calculus as defined by Church, where renaming is an explicit reduction step, on a par with beta-reduction. I also answer a listener's question about what "computational type theory" means.

    Feel free to email me any time at aaron.stump@bc.edu, or join the Telegram group for the podcast.

    Voir plus Voir moins
    20 min
  • POPLmark Reloaded, Part 2

    POPLmark Reloaded, Part 2
    Dec 23 2024

    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.
    Voir plus Voir moins
    14 min

Ce que les auditeurs disent de Iowa Type Theory Commute

Moyenne des évaluations de clients

Évaluations – Cliquez sur les onglets pour changer la source des évaluations.

Évaluations sur Audible.ca

Évaluations sur Amazon.ca
Il n'y a pas encore de critiques pour ce titre.