Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Feb 19, 2025

• Fix CPS translation files (WIP)

  takanuva

  committed
  72ed517

  Copy full SHA for 72ed517

Commits on Oct 7, 2024

• Refactor lambda files to use sigma library

  takanuva

  committed
  6bf7526

  Copy full SHA for 6bf7526

Commits on Apr 26, 2024

• Add pairs and thunks in the lambda calculus syntax

  takanuva

  committed
  0154d89

  Copy full SHA for 0154d89

Commits on Apr 17, 2024

• Add typing annotation to CBV CPS rules

  takanuva

  committed
  b70b83a

  Copy full SHA for b70b83a

Commits on Feb 10, 2024

• Add proof of type preservation for CBV (close enough)

  takanuva

  committed
  34e5e13

  Copy full SHA for 34e5e13

• Sketch SN for CBV from the CPS translation

  takanuva

  committed
  20c2634

  Copy full SHA for 20c2634

Commits on Feb 7, 2024

• Some sketches about the idea of an essential step (WIP)

  takanuva

  committed
  f27d6c9

  Copy full SHA for f27d6c9

Commits on Feb 2, 2024

• Start proof that CBN simulates substitution

  takanuva

  committed
  32e0065

  Copy full SHA for 32e0065

• State preservation of strong normalization to the CBV calculus

  takanuva

  committed
  40c2718

  Copy full SHA for 40c2718

• Show denotational soundness for the CBV calculus

  takanuva

  committed
  c72bbf2

  Copy full SHA for c72bbf2

• Show that the CBV CPS translation is compositional

  takanuva

  committed
  d2de554

  Copy full SHA for d2de554

• Add adequacy theorem for CBV

  takanuva

  committed
  9ccb361

  Copy full SHA for 9ccb361

• Prove half of the adequacy result for CBV

  takanuva

  committed
  de9c87b

  Copy full SHA for de9c87b

• Show that if CBV terminates, then it is strongly normalizing

  takanuva

  committed
  4cddd0c

  Copy full SHA for 4cddd0c

• State normal form preservation for CBV

  takanuva

  committed
  f25f5b6

  Copy full SHA for f25f5b6

• Finish proof for CBV termination

  takanuva

  committed
  d56d15a

  Copy full SHA for d56d15a

• Even more progress on proof of CBV termination

  takanuva

  committed
  4246dcf

  Copy full SHA for 4246dcf

• Some more progress on termination for CBV (we're over 20.000 lines, yeey)

  takanuva

  committed
  a8e4f96

  Copy full SHA for a8e4f96

• Further progress on proof for CBV termination

  takanuva

  committed
  5315ff4

  Copy full SHA for 5315ff4

• Progress on proof of termination for CBV

  takanuva

  committed
  a4bc50b

  Copy full SHA for a4bc50b

• Sketch full simulation for compatible beta-v reduction

  takanuva

  committed
  1e99c1e

  Copy full SHA for 1e99c1e

• Start proof of CBV simulation

  takanuva

  committed
  267b0e5

  Copy full SHA for 267b0e5

Commits on Jan 28, 2024

• Prove the CBV CPS translation preserves and reflects free variables

  takanuva

  committed
  5334911

  Copy full SHA for 5334911

• Add quick inversion lemma for CBV CPS translation and lifting

  takanuva

  committed
  8b70a6f

  Copy full SHA for 8b70a6f

• Show that the CBV CPS translation is total

  takanuva

  committed
  68abb15

  Copy full SHA for 68abb15

• Prove that closed CBV-normal terms have to be values

  takanuva

  committed
  75824dc

  Copy full SHA for 75824dc

• Show CBV reduction is decidable

  takanuva

  committed
  c2a3a02

  Copy full SHA for c2a3a02

Commits on Dec 31, 2023

• Rename files for Plotkin's translations

  takanuva

  committed
  8472057

  Copy full SHA for 8472057

Loading