wilbowma

#lang s-exp "redex-lang.rkt"

(axiom x : Nat)
(axiom y : Nat)

(lambda ((x : Nat)) y)

((lambda ((x : Nat)) y) 0)

; type error

wilbowma

#lang s-exp "interp.rkt"

(define f (lambda (x) #t))
(f #f)

typesanitizer

Here is a list of resources that I have read either fully, or at least to an extent with which I am comfortable with endorsing them.

I've used these resources in different ways:

• Direct application: Some bits and pieces of advice can be applied very directly.
• Reflection: For organizational things, sometimes I would try to write down how I felt my work environment mirrored, and how it differed from the situation described in some work. Writing things down is a useful forcing function to think clearly.
• 1:1 discussions with my manager: We'd take the first 15-20 minutes of

Nikolaj-K

In this video we come across about 50 online resources for category theory:

https://youtu.be/hEW42ARKNoE

I quickly comment on about 20 major ones. I link to the university sites, arXiv sites or Amazon page - most of the mentioned books are online available.

Here's another category theory list on github

https://github.com/prathyvsh/category-theory-resources

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

mort3za

# Generate a new pgp key: (better to use gpg2 instead of gpg in all below commands)
gpg --gen-key
# maybe you need some random work in your OS to generate a key. so run this command: `find ./* /home/username -type d | xargs grep some_random_string > /dev/null`

# check current keys:
gpg --list-secret-keys --keyid-format LONG

# See your gpg public key:
gpg --armor --export YOUR_KEY_ID
# YOUR_KEY_ID is the hash in front of `sec` in previous command. (for example sec 4096R/234FAA343232333 => key id is: 234FAA343232333)

grav

Install VirtualBox (eg on Mac: brew cask install virtualbox)

Download Debian 3.1 from here: https://virtualboxes.org/images/debian/

Create a new VM in VirtualBox and select the vdi file from the above archive as a disk. Check the VM settings:

• Make sure the disk is mounted as an IDE device, SATA errors out on boot (in the Storage tab)
• Also, make sure the pointing device is set to PS/2 Mouse (in the General tab)

elizabrock

Great Papers in Computer Science

19th Century

Lovelace, Ada Augusta (1842) "Notes on the Analytical Engine"

1930's

Aiken, Howard (1937) "Proposed Automatic Calculating Machine"

dergachev

OS X Screencast to animated GIF

This gist shows how to create a GIF screencast using only free OS X tools: QuickTime, ffmpeg, and gifsicle.

Instructions

To capture the video (filesize: 19MB), using the free "QuickTime Player" application:

samth

Emails from Matthew

http://lists.racket-lang.org/users/archive/2005-August/009483.html

http://lists.racket-lang.org/users/archive/2005-November/010350.html

http://lists.racket-lang.org/users/archive/2006-June/013819.html

http://lists.racket-lang.org/users/archive/2006-August/014439.html