Reading List

Contents

• Mathematics
• Logic
  • Automated Theorem Proving
• Programming
  • Algorithms
  • Clojure
  • D
  • Haskell
  • Java Virtual Machine
• 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

Programming

• Bartosz Milewski's Blog

Algorithms

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

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.

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.

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.