Basic notions of Lambda calculus

$\alpha$-conversion changes names of bound variables to fresh ones before substitution. $\alpha$-equivalence equates formulas that differ only in the naming of bound variables. Note that we consider two normal forms to be equal if they are $\alpha$-equivalent.

$\beta$-reduction applies a $\lambda$-term to another term: $(\lambda x.\, e)\ e' \mapsto e\ [e'/x]$. Two expressions are $\beta$-equivalent, if they can be $\beta$-reduced into the same expression.

$\eta$-conversion converts between $λx.(f\ x)$ and $f$ whenever $x \not\in FV(f)$. It expresses the ideas that two functions are the same if and only if they give the same result for all arguments. Hence a function and its eta-conversion is $\eta$-equivalent. In FP, we usually use $\eta$-conversion to bound free variables inside an expression, e.g., to convert $e: A\rightarrow B \rightarrow C$ to $\lambda x.\lambda y.e$.

$\eta$-conversion (together with rule $M \equiv N \implies M\ x \equiv N\ x$) yields the Extensional Principle: $M\ x \equiv N\ x \implies M\equiv N$, given that $x\not\in FV(M)\cup FV(N)$. This principle expresses the lambda calculus form of the notion of extensional equality for functions. That is, two functions $f, g: A\rightarrow B$ are indistinguishable iff $f\ x \equiv g\ x$ for all $x:A$.

The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, $(λx.M)\ N$ is a beta-redex, and $λx.M\ x$ is an $eta$-redex if $x$ is not free in $M$. The expression to which a redex reduces is called its $reduct$. Using the previous example, the reducts of these expressions are respectively $M[N/x]$ and $M$.

GoLang tutorials and resources

http://www.youtube.com/watch?v=MzYZhh6gpI0
A short talk on the essentials of Golang by its creator Russ Cox

http://tobegit3hub1.gitbooks.io/understanding-linux-processes/
Learning Linux processes with Golang examples

Structure and Interpretation of Computer Programs

Full text, source codes, and materials: http://mitpress.mit.edu/sicp/

Scheme resources

Chicken Scheme
http://wiki.call-cc.org/

Racket (PTL Scheme)
http://racket-lang.org/

MIT Scheme
http://www.gnu.org/software/mit-scheme/

Rewriting rules for Scheme evaluation:
http://courses.csail.mit.edu/6.044/fall96/handouts/H14-Scheme-rewriting-model-2.ps
http://courses.csail.mit.edu/6.044/fall96/ftp-dir-fall-95/rewriting-model-1.ps

CoffeeScript and LiveScript

I am familiar with JavaScript, and I am interested in CoffeeScript and LiveScript. I really need some good tutorials before I get enough brevity to use them in my projects.

Functional Programming in JavaScript using LiveScript and prelude.ls

Clojure resources

Learning category theory in Clojure:  http://www.clojure.net/archive.html

For Python Beginners

Why Python?
http://www.linuxjournal.com/article/3882

Bruce Eckel's viewpoints on Python:
http://www.google.com/custom?domains=Artima.com&q=Bruce+Eckel+Python&sa=Search&sitesearch=Artima.com

A Chinese tutorial for Python 3:
http://sebug.net/paper/books/dive-into-python3/

Resources for programming languages

Rust
Rust, an Anti-Sloppy Programming Language
Rust Borrow and Lifetimes

JavaScript
Douglas Crockford: "Crockford on JavaScript -- Scene 6: Loopage" (52 min.)

Node.js
Why node.js is Cool

Algorithms and complexity theory
The Art Gallery Guardian