Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

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

7 views
Skip to first unread message

secr...@lxny.org

unread,
Oct 11, 2016, 1:27:07 AM10/11/16
to
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 <secr...@lxny.org>
Corresponding Secretary LXNY
LXNY is New York's Free Computing Organization.
http://www.lxny.org

0 new messages