Unrated Resources
Unrated Webpages
Systems Theory
- Leverage Points: Places to Intervene in a System - The Donella Meadows Project
- How Complex Systems Fail
- LOOPY: a tool for thinking in systems
Unrated Books
Agile Development
- Agile Systems Engineering (borrow @ archive.org)
Artificial Intelligence
- Building Problem Solvers (borrow @ archive.org)
Category Theory
- Categories, types, and structures (online @ www.di.ens.fr) (borrow @ archive.org)
Chaos Theory
- Chaos: Making a New Science (borrow @ archive.org)
Computational Complexity
- Computational Complexity (Wagner and Wechsung) (borrow @ archive.org)
Coq
- Certified Programming with Dependent Types (online @ archive.org)
- Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) (online @ www.ps.uni-saarland.de)
Formal Language
- Programs, Grammars, Arguments (online @ archive.org)
Forth
- Starting Forth (online @ www.forth.com, archive.org)
- Thinking Forth (online @ www.forth.com)
Functional Programming
- Structure and Interpretation of Computer Programs (online @ archive.org (2nd ed.), archive.org (2nd ed. HTML)) (borrow @ archive.org (1st ed.))
- Purely Functional Data Structures (online @ archive.org)
Lambda Calculus
- Introduction to Combinators and the Lambda Calculus (borrow @ archive.org)
Literature
- The Secret Agent (online @ gutenberg.org)
- The Good Soldier (online @ gutenberg.org)
- The Counterfeiters (online @ archive.org) (borrow @ archive.org) (borrow with print disabilities @ archive.org)
- Mr Pye (borrow @ archive.org)
Logic
- Logic (Hodges) (borrow @ archive.org)
- Mathematical logic and formalized theories (borrow @ archive.org)
- The Blackwell Guide To Philosophical Logic (online @ archive.org)
- Handbook of Logic in Computer Science, Volume 1 (borrow @ archive.org)
- Handbook of Logic and Proof Techniques for Computer Science (borrow @ archive.org)
- Handbook of logic in artificial intelligence and logic programming, Vol 1 (borrow @ archive.org)
- Handbook of logic in artificial intelligence and logic programming, Vol 2 (borrow @ archive.org)
- Handbook of logic in artificial intelligence and logic programming, Vol 4 (borrow @ archive.org)
Logic Programming
- Programming with Higher-Order Logic (borrow @ archive.org)
Mathematics
- Compactness and Contradiction (online @ terrytao.wordpress.com)
PLDI
- Threaded Interpretive Languages (online @ archive.org)
Partial Evaluation
- Partial Evaluation and Automatic Program Generation (online @ www.itu.dk)
Proof Theory
- Basic Proof Theory (borrow @ archive.org)
Refinement Calculus
- a Practical Theory of Programming (online @ www.cs.toronto.edu)
- Refinement Calculus: A Systematic Introduction (online @ lara.epfl.ch)
Theory of Computation
- Theory of Recursive Functions and Effective Computability (borrow @ archive.org)
- Computability Theory, Semantics, and Logic Programming (borrow @ archive.org)
Type Theory
- Basic Simple Type Theory (borrow @ archive.org)
- Type Theory and Functional Programming (online @ www.cs.kent.ac.uk)
- Programming in Martin-Löf’s Type Theory (online @ www.cse.chalmers.se)
x86
- 80386 -- A Programming and Design Handbook (borrow @ archive.org)
- The x86 PC (borrow @ archive.org)
- IA-64 for Software Developers (borrow @ archive.org)
- PC Assembly Book (online @ pacman128.github.io)
Unrated Papers
Abstract Algebra
Computational Complexity
- Complexity Hierarchies Beyond Elementary (online @ arxiv.org)
- Pure vs Impure Lisp (online @ dl.acm.org)
Coq
- Recursive Datatypes and Inductive Proofs (online @ www.inf.ed.ac.uk)
- Interactive Theorem Proving with Coq (online @ people.eecs.berkeley.edu)
Formal Specification
- Consistency Checking of Functional Requirements
- Consistency Checking in Requirements Analysis
- Automated Consistency Checking of Requirements Specifications
Functional Programming
- let (rec) insertion without effects, lights or magic (online @ icfp19.sigplan.org)
Incompleteness
- A Simple Character String Proof of the \"True but Unprovable\" Version of Goedel\'s First Incompleteness Theorem (online @ arxiv.org)
- A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points (online @ arxiv.org)
- Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles (online @ jstor)
Lambda Calculus
Macros
- Hygiene for the Unhygienic (online @ www.p-cos.net, guenchi.github.io)
- Binding as Sets of Scopes
Modal Logic
- Modal Mu-Calculi (online @ www.julianbradfield.org)
Name Binding
- A Type and Scope Safe Universe of Syntaxes with Binding
- Don’t Substitute Into Abstractions (Functional Pearl)
- Viewing λ-terms through Maps
Refinement Calculus
Relational Programming
Term Rewriting
Theorem Proving
- From LCF to HOL (online @ www.cl.cam.ac.uk)
- Towards self-verification of HOL Light (online @ www.cl.cam.ac.uk)
- A Self-Verifying Theorem Prover (online @ www.kookamara.com)
Type Theory
- Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega (online @ web.cs.ucla.edu)