NYC LOCAL: Tuesday 11 October 2016 Lisp NYC: Jay Sulzberger on FizzBuzz, mutilated chessboards, and the Dream of Homotopy Type Theory

NYC LOCAL: Tuesday 11 October 2016 Lisp NYC: Jay Sulzberger on FizzBuzz, mutilated chessboards, and the Dream of Homotopy Type Theory

[secretary]

Lisp NYC, http://lispnyc.org, will meet on

  Tuesday 11 October 2016 at
  1900 hours at

  Shareablee
  123 William Street, 19th Floor
  near Wall Street, on the Island of the Manahattoes

  Subway stations:

  Fulton Street on the 2, 3, 4, 5, A, C, and J, lines.
  The schedule of the Z line is obscure to me.
  There are other lines which stop nearby.

  Though the formal RSVP door is closed, I say show up and
  we will make every effort to get you in, consistent with
  New York City Fire Regulations.


Here are two more titles for the talk:

  On the Several Differences between Lisp and the Lambda Calculus,

  The Paradigm Case of Curry-Howard [that is, for the Simply
  Typed Lambda Calculus] Helps Tell When Two Proofs of a Given
  Proposition are Really The Same.


WARNING: This talk is, in large part, the result of my failure
to grasp material in the Big HoTT Book, and my positive
misunderstandings of elementary Type Theory.  I thank
Noson Yanofsky, in particular, and all the participants
in the Homotopy Type Theory and More CUNY Seminar for their
long continued efforts to teach me the basics.

Here is the page for the seminar:

http://www.sci.brooklyn.cuny.edu/~noson/CTseminar.html


  Background reading:

  Noson Yanofsky's papers on Programs and Algorithms, and on
  various equivalence relations on these two collections:

  https://arxiv.org/abs/math/0602053
  https://arxiv.org/abs/1011.0014


  On FizzBuzz:

  https://en.wikipedia.org/wiki/Fizz_buzz
  [page was last modified on 27 September 2016, at 08:09]

  https://www.rosettacode.org/wiki/FizzBuzz


  Gian-Carlo Rota's note on Alonzo Church:

  https://www.princeton.edu/mudd/finding_aids/mathoral/pmcxrota.htm


  When are two proofs the same?:

  http://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs

  http://math.stackexchange.com/questions/1242043/when-are-two-proofs-the-same

  https://gowers.wordpress.com/2007/10/04/when-are-two-proofs-essentially-the-same/

  https://homotopytypetheory.org/

  https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/

  https://en.wikipedia.org/wiki/Cryptomorphism
  [page was last modified on 15 March 2013, at 22:24]


  And more:

  Physics, Topology, Logic and Computation: A Rosetta Stone
  by John C. Baez and Mike Stay:

  https://arxiv.org/abs/0903.0340


  Lectures on the Curry-Howard Isomorphism, May 1998 not final version
  by M. H. B. Sorenson and P. Urzyczyn:

  http://www.dcc.fc.up.pt/~nam/aulas/0405/tia/lectures-on-the-curry.pdf


  Tom Stuart's delightful "Programming with Nothing":

  http://codon.com/programming-with-nothing


  J. R. Hindley's 1997 book Basic Simple Type Theory:

  https://mathtrielhighschool.files.wordpress.com/2011/08/number-theory.pdf


  Oleg of Okmij's calculators:

  http://okmij.org/ftp/Computation/lambda-calc.html


  Jan Malakhovski's propaganda for taking seriously certain
  logical difficulties with material implication:

  http://oxij.org/note/ReinventingFormalLogic/


Distributed poC TINC:

Jay Sulzberger <secretary@lxny.org>
Corresponding Secretary LXNY
LXNY is New York's Free Computing Organization.
http://www.lxny.org