POPLmark Reloaded, Part 2

Update: 2024-12-23

Description

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.

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-176435118088423{-webkit-line-clamp:2;}POPLmark Reloaded, Part 2

POPLmark Reloaded, Part 2

Aaron Stump

POPLmark Reloaded, Part 2