# links

## 1 Programming

### 1.1 Languages

### 1.2 Functional programming

- Lambda the Ultimate - a lot of news, links, and reviews sometimes
- The Comonad.Reader

### 1.3 Blogs and homepages

- John McCarthy's Home Page
- call-with-current-musing
- John Cowan's Home Page and his blog
- synthcode: some software (including chibi scheme and irregex), a blog, and some more materials
- Xah Code - a lot of information about Emacs, keyboards, and other stuff
- Wisdom and Wonder
- λ Tony's blog λ
- wingolog
- Things that amuse me
- oxij
- puffnfresh blog
- Conor McBride's site
- raichoo : λΠ-punk
- David Christiansen blog
- Existential Type
- tailcalled
- Hackery, Math & Design
- Christian Neukirchen's web site, including blog and nice links/feeds collection
- Chris Done's Homepage
- The Wisdom of James Mickens

### 1.4 Other

#### 1.4.1 Collections

- Great Works in Programming Languages (collected by Benjamin C. Pierce)
- a few more collections at http://homes.cs.washington.edu/~csgordon/#reading
- Programming Language Research
- steshaw/plt-study
- bitemyapp/learnhaskell

#### 1.4.2 Programming exercises

- exercism.io
- Timus Online Judge
- VerifyThis, "A collection of verification benchmarks"
- Project Euler
- Logitext "is an educational proof assistant for first-order classical logic using the sequent calculus"

#### 1.4.3 Publications

- CSAIL Publications - a lot of AI-related publications
- Fentic Publications - some SDN-related publications

#### 1.4.4 Misc

## 2 Entertainment

### 2.1 Comics

- XKCD:
*A webcomic of romance, sarcasm, math, and language.* - Existential comics:
*A philosophy comic about the inevitable anguish of living a brief life in an absurd world. Also jokes.* - Invisible Bread: there's an invisible bread in the lower-right corner.
- Saturday Morning Breakfast Cereal

### 2.2 Videos

- They're Made Out of Meat: a short video by this short story
- Adulting
- I did it!

## 3 Books

Probably I'll try to backup all this and replace it with links to files later.

### 3.1 Technical

It's not easy to list all the nice books, or even to decide which books to list, but here are some.

- Programming Languages: Application and Interpretation: nice and relatively short/simple introductory book about interpreters (including typing), a video linked from its introduction is nice also.
- The Unix-Haters Handbook: funny and interesting book, as far as I can tell after reading first 70 pages.
- Type Theory and Functional Programming - it has explicit enough title, the book is nice.
- Types and Programming Languages - the same topic.
- Software Foundations: similar subject, with exercises and examples in Coq. Works fine as reader's first book on topic of formal theorem proving.
- SICP - this one is quite popular, but will link it from here anyway.
- Dragon Book - widely known also, but linking too; this (the "Red" one), together with SICP, made me look at programming from a [one more] different side.
- The HoTT Book + prerequisites and helpful materials:
- Topology by Munkres
- Algebraic Topology by Hatcher
- Higher Inductive Types: a tour of the menagerie
- CW complexes
- CW Defn and Examples
- Wikipedia and SO are helpful, too

- Conceptual Mathematics: A First Introduction to Categories
- Andrew S. Tanenbaum's books: pretty lengthy, but very readable, and can be used as references.
- Lang's books for algebra, though they are not that easy to read.

### 3.2 Non-technical

Same situation as with technical books; just writing here something, without any defined system.

- Gödel, Escher, Bach: have not read it yet, but probably an interesting book.
- The Neverending Story: I have heard that it is an interesting book, but have a dozen of recommended books enqueued, so not sure if/when will try this one.
- A Brief History of Time – a short pop-science book.

## 4 Articles

Links to articles are dying surprisingly fast, I should fix them somehow.

### 4.1 Programming-related

#### 4.1.1 Parsing/printing

#### 4.1.2 DTLC

- Simpler, Easier!
- Pi-Forall + corresponding lectures
- ΠΣ: Dependent Types without the Sugar
- nano-Agda
- A tutorial implementation of a dependently typed lambda calculus
- How to implement dependent type theory I

#### 4.1.3 GADTs, (Co)inductive types, CciC

- Co-Logic Programming: Extending Logic Programming with Coinduction
- Coinductive Logic Programming and its Applications
- The Algebra of Data, and the Calculus of Mutation
- CPDT chapters: Inductive Types, Coinductive
- Termination Checking Nested Inductive and Coinductive Types
- Wellfounded Recursion with Copatterns
- MiniAgda: Integrating Sized and Dependent Types
- A predicative analysis of structural recursion
- Termination Checking Nested Inductive and Coinductive Types
- Pattern matching without K
- Elimination with a Motive

#### 4.1.4 Functional programming

#### 4.1.5 Programming with dependent types

#### 4.1.6 Session types

It's useful to read about π-calculus (FAQ on π-Calculus) before reading about session types. λ-calculus knowledge is assumed, as pretty much in any other linked article here, and general familiarity type theories. Materials are ordered by complexity, from basic introduction to more advanced ones.

#### 4.1.7 Unsorted

trx : Regular-tree expressions, now in Scheme:

Regular-tree expressions are to semi-structured data, such as XML and Lisp s-expressions, what standard regular expressions are to strings

- What Every Computer Scientist Should Know About Floating-Point Arithmetic; And there's also a nice wiki article: it's always better to know and remember such little things.
- Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932)
- F. Cardone and J. R. Hindley, History of Lambda-Calculus and Combinatory logic (2006)

### 4.2 UNIX-related

### 4.3 Graphics and typography

- On the typography of flight-deck documentation (NASA contractor report # 177605)
- Color Graphics, also by NASA, and includes topics like legibility

### 4.4 Non-technical

### 4.5 Other

## 5 Other

### 5.1 Food

- Soylent
- The Flavor Connection
- Supercook - a fine recipe search
- openrecipes - a food recipes database
- SimplyRecipes - some recipes, too

### 5.2 Emergency exit

- lostallhope.com - a good site with statistics, method descriptions and references
- The Peaceful Pill Handbook
- Final Exit - reference, various materials
- Dignitas - assisted suicide services for terminally ill
- How to kill a human being (a BBC documentary film)
- Suicide methods, a Wikipedia article
- A protocol for dying

### 5.3 Misc

- Lojban
- Lamdu
- CosmicOS
- suckless.org
- SDF Public Access UNIX System
- tilde.club
- Dedoimedo: "A place to learn a lot about a lot!" (software, in particular)
- Schneier on Security
- Off-the-Record Messaging
- StanfordUniversity on youtube, and Robert Sapolsky lectures in particular – quite interesting, as pop-sci.
- Theorem of the Day
- Privacy tools