Unrated Resources
Unrated Books
Agile Development
- Agile Systems Engineering (borrow with print disabilities @ archive.org)
Artificial Intelligence
- Building Problem Solvers (borrow with print disabilities @ archive.org)
BASIC
- True BASIC by Problem Solving (online @ archive.org)
- Jt's Conversations on True Basic (Mac) (borrow @ archive.org)
- Jt's Conversations on True BASIC (Windows) (borrow @ archive.org)
Category Theory
- Categories, types, and structures (online @ www.di.ens.fr) (borrow @ archive.org)
Comics
- Krazy Kat (borrow @ archive.org)
- Krazy Kat: The Comic Art of George Herriman (borrow @ archive.org)
Computer Security
- Security Engineering (online @ www.cl.cam.ac.uk)
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)
JavaScript
- The Principles of Object-Oriented JavaScript (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)
- Stand on Zanzibar (borrow @ archive.org) (borrow with print disabilities @ 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) (borrow with print disabilities @ archive.org)
- Handbook of Logic in Computer Science, Volume 1 (borrow @ archive.org)
Logic Programming
- Programming with Higher-Order Logic (borrow with print disabilities @ archive.org)
Mathematics
- Compactness and Contradiction (online @ terrytao.wordpress.com)
Order Theory
- Lattices to Logic (borrow @ archive.org)
- Introduction to Lattices and Order (borrow @ archive.org)
PLDI
- Threaded Interpretive Languages (online @ archive.org)
- Programming Language Pragmatics (borrow @ archive.org, archive.org, archive.org)
Partial Evaluation
- Partial Evaluation and Automatic Program Generation (online @ www.itu.dk)
Probability Theory
- Bayesian Reasoning and Machine Learning (borrow @ archive.org)
Python
- Python Scripting for Computational Science (borrow @ archive.org)
Reactive Systems
- A Practical Introduction To Real-Time Systems For Undergraduate Engineering (online @ archive.org)
Refinement Calculus
- a Practical Theory of Programming (online @ www.cs.toronto.edu)
- Refinement Calculus: A Systematic Introduction (online @ lara.epfl.ch)
Theorem Proving
- Hyperproof (borrow @ archive.org)
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 with print disabilities @ 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
- 80286 Assembly Language on MS-DOS Computers (borrow @ archive.org)
- 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
- The Convolution Algebra
- Algebras and combinators
- Algebras and combinators (Algebra universalis 1981)
- Equations in Combinatory Algebras
- Higher-Order Algebraic Theories
Category Theory
- Physics, Topology, Logic and Computation: A Rosetta Stone (online @ arxiv.org)
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)
Equational Logic
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)
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
- A nominal axiomatisation of the lambda-calculus
Public Domain
- Abandoning Copyright (online @ papers.ssrn.com)
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)
Theory of Computation
- Unpredictability and Undecidability in Dynamical Systems (online @ gwern.net, scribd.com)
- Decidability and Undecidability in Dynamical Systems (online @ inria.hal.science)
Type Theory
- Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega (online @ web.cs.ucla.edu)