Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 22, 2022

• Update README.md

  bafain

  committed
  0768c86

  Copy full SHA for 0768c86

Commits on Feb 4, 2022

• Add slides from Peter's talk

  carlostome

  committed
  5bd9cae

  Copy full SHA for 5bd9cae

Commits on Nov 26, 2021

• Merge pull request #9 from InitialTypes/carlostome-patch-1

  andreasabel

  authored
  c23327f

  Copy full SHA for c23327f

Commits on Nov 25, 2021

• Update nbe-ipl.md

  carlostome

  authored
  d3911e2

  Copy full SHA for d3911e2

• Change Nf to enforce that normal proofs of negative type start with an intro rule

  carlostome

  authored
  576c613

  Copy full SHA for 576c613

• Lecture on IPL: clarification

  bafain

  committed
  3677e92

  Copy full SHA for 3677e92

• Lecture on IPL: typos

  bafain

  committed
  61d63c3

  Copy full SHA for 61d63c3

• Lecture on IPL

  andreasabel

  committed
  88ec15d

  Copy full SHA for 88ec15d

Commits on Nov 15, 2021

• Newman's lemma: solutions, and undo one nitpick

  andreasabel

  committed
  9dd25be

  Copy full SHA for 9dd25be

Commits on Nov 8, 2021

• update thesis

  wmacmil

  authored
  c8405a8

  Copy full SHA for c8405a8

• Delete GrammarOfProof.pdf

  wmacmil

  authored
  d6c7b22

  Copy full SHA for d6c7b22

• [ reduction ] Code: Make the successor redexes that expDoneInCtx? picks explicit

  bafain

  committed
  21f42cf

  Copy full SHA for 21f42cf

• [ reduction ] Code: Reduction as given by EvalCtx and ∼ is nondeterministic

  bafain

  committed
  bf89305

  Copy full SHA for bf89305

• [ reduction ] Code: Module SetoidReasoning is deprecated

  bafain

  committed
  936b977

  Copy full SHA for 936b977

Commits on Nov 6, 2021

• Introductory exercise: Confluence implies Church–Rosser

  bafain

  committed
  900a95e

  Copy full SHA for 900a95e

Commits on Nov 5, 2021

• Newman's lemma: nitpicks

  bafain

  committed
  9a3d42f

  Copy full SHA for 9a3d42f

• [ reduction ] Add code from session on reduction

  nachivpn

  committed
  6e57fdb

  Copy full SHA for 6e57fdb

Commits on Nov 4, 2021

• Advanced exercise: Newman's lemma

  andreasabel

  committed
  b698948

  Copy full SHA for b698948

Commits on Oct 18, 2021

• Move Nachi's code to separate folder

  bafain

  committed
  da7c425

  Copy full SHA for da7c425

Commits on Sep 30, 2021

• [ ccc ] Add exercise 6.14 from Awodey in Agda

  

  carlostome

  authored and

  bafain

  committed
  249d7af

  Copy full SHA for 249d7af

Commits on Sep 23, 2021

• [ ccc ] Update PDFs

  

  sstucki

  authored and

  bafain

  committed
  ba2baa0

  Copy full SHA for ba2baa0

• [ ccc ] Apply notes on notes of today's ITC lecture

  Show description for be3b87c
  

  sstucki

  authored and

  bafain

  committed
  be3b87c

  Copy full SHA for be3b87c

• [ ccc ] updated PDFs

  andreasabel

  committed
  543fdaa

  Copy full SHA for 543fdaa

• [ ccc ] Add some examples and motivation.

  andreasabel

  committed
  3c5d68a

  Copy full SHA for 3c5d68a

Commits on Sep 17, 2021

• Update slides for STLC-CCC lecture 1.

  sstucki

  committed
  3fcbb37

  Copy full SHA for 3fcbb37

Commits on Sep 8, 2021

• [grammar-proof] Add Warrick's thesis

  nachivpn

  committed
  722a006

  Copy full SHA for 722a006

Commits on Sep 3, 2021

• Update README.md

  bafain

  committed
  a8a4a4d

  Copy full SHA for a8a4a4d

Commits on May 25, 2021

• [ parametricity ] predicative F: more comments, clean out flawed ICFP 2020 proof

  andreasabel

  committed
  a21a580

  Copy full SHA for a21a580

• [ parametricity ] predicative F: comments and clean up (up to Terms)

  andreasabel

  committed
  8ced915

  Copy full SHA for 8ced915

Commits on May 21, 2021

• [ parametricity ] predicative F: clean up; Peirce is not parametric

  andreasabel

  committed
  26b2fee

  Copy full SHA for 26b2fee

• [ parametricity ] WIP: predicative F: proved the Wadler free theorem

  Show description for bec1bb7
  andreasabel

  committed
  bec1bb7

  Copy full SHA for bec1bb7

• [ parametricity ] WIP: predicative F: setoid hell

  andreasabel

  committed
  8f726c1

  Copy full SHA for 8f726c1

• [ parametricity ] WIP: predicative F: full reduction for subst propagation

  andreasabel

  committed
  22f007e

  Copy full SHA for 22f007e

Commits on May 20, 2021

• [ parametricity ] WIP: predicative F with expl substs (missing some conv)

  andreasabel

  committed
  efee4f8

  Copy full SHA for efee4f8

• [ parametricity ] WIP: predicative F with explicit substitutions

  andreasabel

  committed
  135215b

  Copy full SHA for 135215b

Pagination

Previous

Next