Unrated Resources

Unrated Webpages

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

• The Convolution 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

• On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control

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

• Program Derivation by Correctness Enhancements

Relational Programming

• Relational programming

Term Rewriting

• The Rho Cube

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)

Unrated Repositories