Tuesday, December 4, 2018

12/4/18: The Path Forward

We took a quick look today at the Nat-Nat problems, and in particular around the distinction between + and plus. But the main conversation was over what to do next quarter. The current plan is some combination of learning linear logic (anyone know of great references?!) and blodwen, as the later makes (or at least, is demonstrated to make, which isn't quite the same thing) effective use of linearity constraints in its types.

at

1 comment:

  1. KartikDecember 8, 2018 at 6:59 PM

    Learning linear logic sounds like a great idea, I will be super interested (makes sense for quantum computing's no-cloning theorem). I attended these lectures by Paul Downen at the last OPLSS, which might serve as a good intro:

    Videos: https://www.youtube.com/playlist?list=PL0DsGHMPLUWWoK7s-j0yGKRThT6bRkxp-

    Notes: https://www.cs.uoregon.edu/research/summerschool/summer18/lectures/foundations_notes.pdf (Ch-8, 9)

    ReplyDelete

Subscribe to: Post Comments (Atom)

12/4/18: The Path Forward

We took a quick look today at the Nat-Nat problems , and in particular around the distinction between + and plus . But the main conversatio...

  • Our First Meeting
    At our first meeting, we agreed to read “The Little Typer” through Chapter 4 (but read below), and seriously outgrew our space, with twe...
  • 12/4/18: The Path Forward
    We took a quick look today at the Nat-Nat problems , and in particular around the distinction between + and plus . But the main conversatio...
  • Nat-Nat Problems
    Problem 1 . Write the functions max and monus , where (claim max (-> Nat Nat Nat)) is the usual max function, e.g., ...