Reading List

Contents

• Mathematics
• Logic
  • Automated Theorem Proving
• Operating Systems
• Programming
  • Algorithms
  • C++
  • Clojure
  • D
  • Haskell
  • Java Virtual Machine
  • Lisp
• Hardware
• Literature

Mathematics

• Kan Extension Seminar reading group about category theory papers.

Logic

• QA9 is a fascinating "computational logic" blog.

Automated Theorem Proving

Despite its name, it's really "Treat math like a programming language, and if the 'program' 'compiles' then the proofs are true." But the field sounds like "ZOMG! Skynet!"

• Wiedijk's preprint on the Mathematical Vernacular [pdf]
• Carnegie Mellon's Course "15-815 Automated Theorem Provers" Lecture Notes
• Introduction to Automated Theorem Proving with Logtk
• Jean Gallier's book Logic for Computer Science: Foundations of Automatic Theorem Proving
• Metatheorem Blog

Operating Systems

Operating systems have two major components at its heart, plus a bunch of really "nice to haves" (like networking): process management, file systems. The former (process management) is really the soul of operating systems (without it, you have no operating system). File systems are a nice-to-have component (you can have an operating system without one).

• A Constructive Look At TempleOS
• xv6
• raspberry-pi-os

See also my Hard Disk Geometry Notes.

Programming

• Bartosz Milewski's Blog
• Let's Build a Simple Database: Writing a sqlite clone from scratch in C

Algorithms

• Algorithmist Wiki a collection of algorithms, and basic analyses thereof...

C++

• C++ Annotations
• C++ Internals

Clojure

• Clojure STM - What? Why? How?
• The Life of a Clojure Expression
• Clojure Compilation: Parenthetical Prose to Bewildering Bytecode

Also see Make a Lisp for the nuts and bolts of making a lisp.

D

• BIOS Boot to D, which contains a fascinating discussion of BIOS and assembly (refers to The Art of Assembly Language for details on the latter)

Haskell

• Code & Co. discusses quite a few fascinating topics (e.g., Types and Kinds and Sorts, Oh My!)
• What I Wish I Knew When Learning Haskell 2.1
• Learning Haskell, a great annotated bibliography of tutorials on Haskell
• Stephen Diehl's Blog has nifty stuff
• Semantic Domain
• Comonad.Reader
• Haskell for All

Articles

• How Lazy Evaluation Works in Haskell
• An Eq instance for non de Bruijn terms

Dependent Types in Haskell

• Dependently typed programming and theorem proving in Haskell

Ebooks on Haskell

• Real World Haskell
• Learn You a Haskell

Java Virtual Machine

• Java Virtual Machine: the Essential Guide
• My assorted collection of links on the JVM's Lambda implementation
• Brian Goetz - "Lambdas in Java: A peek under the hood" , a talk at GOTO Aarhus 2013.
• JVM Internals
• JVM Anatomy Park
• Understanding JVM Internals

Garbage Collection

• Java Memory Management Pragmatics
• Java Garbage Collection Distilled
• Understanding Java Garbage Collection
• Tuning JVM GC for a Big, Mathy, STMful Clojure App

Formalization of the Java Virtual Machine

• J Strother Moore's Formal Model of the JVM Course CS378 at the University of Texas at Austin
• Hanbing Liu, "Formal Specification and Verification of a JVM and its Bytecode Verifier" Doctoral Thesis (2006) Eprint, 332 pages, pdf.
• J. Strother Moore and George Porter, "An Executable Formal Java Virtual Machine Thread Model". In Java Virtual Machine Research and Technology Symposium (JVM '01), USENIX, April, 2001. Eprint
• J. Strother Moore, Robert Krug, Hanbing Liu, George Porter, "Formal Models of Java at the JVM Level: A Survey from the ACL2 Perspective". In Workshop on Formal Techniques for Java Programs, 2001. Eprint, 10 pages.

Lisp

• Paul Graham's On Lisp is a good first book
• Practical Common Lisp
• Peter Norvig's Paradigms of AI is now free online (put online by author)
• Style Guide
  • I dislike the predicate convention (suffix -p for compound names, and suffix p for simple names). I'm more tempted to stick to Clojure's convention (suffix ? for predicates)

Some random blog posts giving opinions and history to Lisp.

• A Road to Common Lisp
  • I disagree with the author's contention that a package could be split across multiple files; it could, but it's bad style (locating an identifier's definition becomes quite a bit harder).
• Some Observations About LISP
• Common Lisp in Practice
• How Lisp Became God's Own Programming Language

Lisp isn't just a language: it's a cult. Err, I mean, way of life.

• StumpWM is a window manager written in Common Lisp
  • Raspberry Pi for Common Lisp Development
  • In the Mood for Lisp, written in 2013, though SBCL now supports ARM
  • Example config
  • Hacking StumpWM with Common Lisp
• Lisp: Good News, Bad News, How to Win Big
• LaTTe is a declarative-style theorem prover (CoC foundations) written in Clojure
  • Challenge: translate the MML to Lispy syntax. (Not necessarily checkable by LaTTe, just change the syntax to use S-expressions)
  • Reference for Mizar Syntax
  • Also the Journal of Formalized Mathematics
• The weaknesses of SBCL's type propagation

Hardware

• Trinity Project apparently trying to build a ternary LISP machine

Literature

Teddy Roosevelt had over 8000 books at Sagamore hill (everything he owned there was indexed). It might make a nice reading list.

Pigskin Library

Here's the contents of Roosevelt's "Pigskin Library". I had trouble finding the exact list, so I'm making note for my future reading.

• Bible.
• Apocrypha.
• George Borrow:
  • Bible in Spain.
  • Zingali.
  • Lavengro.
  • Wild Wales.
  • The Romany Rye.
• Shakespeare: [Comedies. Histories and Poems. Tragedies.]
• Edmund Spenser: Faerie Queene.
• Christopher Marlowe.
• Alfred T. Mahan Sea Power.
• Thomas Babbington Macaulay:
  • History of England. Take with a pillar of salt, Babbington was called one of the greatest systematic falsifier of facts mankind has ever known.
  • Essays.
  • Poems.
• Homer: Iliad and Odyssey.
• Chanson de Roland.
• Nibelungenlied.
• Thomas Carlyle:
  • Frederick the Great.
• Shelley: Poems.
• Francis Bacon: Essays.
• James Russell Lowell:
  • Literary Essays. [Latest Literary Essays.]
  • Biglow Papers.
• Emerson: Poems.
• Longfellow.
• Tennyson.
• Poe:
  • Tales.
  • Poems.
• Keats.
• Milton: Paradise Lost (Books I and II)
• Dante: Inferno (Carlyle's translation)
• Oliver Wendell Holmes, Sr.:
  • Autocrat of the Breakfast Table
  • Over the Teacups.
• Bret Harte:
  • Poems.
  • Tales of the Argonauts.
  • Luck of Roaring Camp.
• Robert Browning: Selections.
• Samuel McChord Crothers:
  • Gentle Reader.
  • Pardoner's Wallet.
• Mark Twain:
  • Huckleberry Finn.
  • Tom Sawyer.
• John Bunyan Pilgrim's Progress.
• Euripides (Murray's translation):
  • Hippolytus.
  • Bacchae.
• The Federalist Papers.
• Gregorovius: History of Rome during the Middle Ages.
• Sir Walter Scott:
  • Legend of Montrose.
  • Guy Mannering.
  • Waverley.
  • Rob Roy.
  • Antiquary.
• James Fenimore Cooper:
  • The Pilot.
  • Two Admirals.
• Froissart's Chronicles.
• Thomas Percy: The Reliques of Ancient English Poetry.
• Thackeray:
  • Vanity Fair.
  • History of Pendennis.
• Dickens:
  • Our Mutual Friend.
  • Pickwick.
• Goethe: Faust.
• Cervantes: Don Quixote (Ormsby's translation)
• Molière.
• Pascal et al.: Pensées.