Nominal Isabelle/HOL

Update: 2025-01-31

Description

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.

Comments

In Channel

Measure Functions and Termination of STLC

2025-11-1421:42

Schematic Affine Recursion, Oh My!

2025-08-2218:49

The Stunner: Linear System T is Diverging!

2025-08-1921:03

Terminating Computation First?

2025-08-0111:27

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

2025-05-1207:10

Krivine's Proof of FD, Using Intersection Types

2025-05-0521:35

A Measure-Based Proof of Finite Developments

2025-04-1623:24

Introduction to the Finite Developments Theorem

2025-03-2715:54

Nominal Isabelle/HOL

2025-01-3116:18

The Locally Nameless Representation

2025-01-0319:54

POPLmark Reloaded, Part 2

2024-12-2313:59

POPLmark Reloaded, Part 1

2024-12-2315:14

Introduction to Formalizing Programming Languages Theory

2024-11-2512:20

Turing's proof of normalization for STLC

2024-05-2117:39

Introduction to normalization for STLC

2024-05-1409:39

The curious case of exponentiation in simply typed lambda calculus

2024-05-0407:29

Arithmetic operations in simply typed lambda calculus

2024-05-0409:56

#box-pro-ellipsis-176440151698313{-webkit-line-clamp:2;}Nominal Isabelle/HOL

Nominal Isabelle/HOL

Aaron Stump

Nominal Isabelle/HOL