Unrated Resources ================= Unrated Books -------------- ### Agile Development * Agile Systems Engineering (borrow with print disabilities @ [archive.org](https://archive.org/details/agilesystemsengi0000doug)) ### Artificial Intelligence * Building Problem Solvers (borrow with print disabilities @ [archive.org](https://archive.org/details/buildingproblems0000forb)) ### BASIC * True BASIC by Problem Solving (online @ [archive.org](https://archive.org/details/brian-d-hahn-true-basic-by-problem-solving)) * Jt's Conversations on True Basic (Mac) (borrow @ [archive.org](https://archive.org/details/jtsconversations0000lloy)) * Jt's Conversations on True BASIC (Windows) (borrow @ [archive.org](https://archive.org/details/isbn_9780757520754)) ### Category Theory * Categories, types, and structures (online @ [www.di.ens.fr](https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf)) (borrow @ [archive.org](https://archive.org/details/categoriestypess0000aspe)) ### Comics * Krazy Kat (borrow @ [archive.org](https://archive.org/details/krazykat00herr_njk)) * Krazy Kat: The Comic Art of George Herriman (borrow @ [archive.org](https://archive.org/details/krazykatcomicart00herr)) ### Computer Security * Security Engineering (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~rja14/book.html)) ### Coq * Certified Programming with Dependent Types (online @ [archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes)) * Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) (online @ [www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf)) ### Formal Language * Programs, Grammars, Arguments (online @ [archive.org](https://archive.org/details/flooved3381)) ### Forth * Starting Forth (online @ [www.forth.com](https://www.forth.com/starting-forth/), [archive.org](https://archive.org/details/LeoBrodieStartingFORTHIntroductionToTheFORTHLanguageAndOperatingSystemForBeginne)) * Thinking Forth (online @ [www.forth.com](https://www.forth.com/wp-content/uploads/2018/11/thinking-forth-color.pdf)) ### Functional Programming * Structure and Interpretation of Computer Programs (online @ [archive.org](https://archive.org/details/StructureAndInterpretationOfComputerProgramsSecondEdition) (2nd ed.), [archive.org](https://archive.org/details/pdfy-x0q2Q4K6h-gsWbes) (2nd ed. HTML)) (borrow @ [archive.org](https://archive.org/details/structureinterpr00abel) (1st ed.)) * Purely Functional Data Structures (online @ [archive.org](https://archive.org/details/okasaki-purely-functional-data-structures)) ### JavaScript * The Principles of Object-Oriented JavaScript (online @ [archive.org](https://archive.org/details/ThePrinciplesOfObjectOrientedJavaScriptNicholasC.Zakas)) ### Lambda Calculus * Introduction to Combinators and the Lambda Calculus (borrow @ [archive.org](https://archive.org/details/introductiontoco0000hind)) ### Literature * The Secret Agent (online @ [gutenberg.org](https://www.gutenberg.org/ebooks/974)) * The Good Soldier (online @ [gutenberg.org](https://www.gutenberg.org/ebooks/2775)) * The Counterfeiters (online @ [archive.org](https://archive.org/details/counterfeiters00gide)) (borrow @ [archive.org](https://archive.org/details/counterfeiterswigide)) (borrow with print disabilities @ [archive.org](https://archive.org/details/counterfeiters0000gide_o3w8)) * Stand on Zanzibar (borrow @ [archive.org](https://archive.org/details/standonzanzibar0000unse)) (borrow with print disabilities @ [archive.org](https://archive.org/details/standonzanzibar00brun)) ### Logic * Logic (Hodges) (borrow @ [archive.org](https://archive.org/details/logic00hodg)) * Mathematical logic and formalized theories (borrow @ [archive.org](https://archive.org/details/mathematicallogi0000roge)) * The Blackwell Guide To Philosophical Logic (online @ [archive.org](https://archive.org/details/lou-goble-the-blackwell-guide-to-philosophical-logic)) (borrow with print disabilities @ [archive.org](https://archive.org/details/blackwellguideto0000unse_q4c2)) * Handbook of Logic in Computer Science, Volume 1 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0001unse_z8j4)) ### Logic Programming * Programming with Higher-Order Logic (borrow with print disabilities @ [archive.org](https://archive.org/details/programmingwithh0000mill)) ### Mathematics * Compactness and Contradiction (online @ [terrytao.wordpress.com](https://terrytao.wordpress.com/wp-content/uploads/2011/06/blog-book.pdf)) ### Order Theory * Lattices to Logic (borrow @ [archive.org](https://archive.org/details/latticestologic00dubi)) * Introduction to Lattices and Order (borrow @ [archive.org](https://archive.org/details/introductiontola0000dave)) ### PLDI * Threaded Interpretive Languages (online @ [archive.org](https://archive.org/details/R.G.LoeligerThreadedInterpretiveLanguagesTheirDesignAndImplementationByteBooks1981)) * Programming Language Pragmatics (borrow @ [archive.org](https://archive.org/details/programminglangu0000scot_4edi), [archive.org](https://archive.org/details/programminglangu0000scot_m3j1), [archive.org](https://archive.org/details/programminglangu0000scot_i7d2)) ### Partial Evaluation * Partial Evaluation and Automatic Program Generation (online @ [www.itu.dk](http://www.itu.dk/people/sestoft/pebook/)) ### Probability Theory * Bayesian Reasoning and Machine Learning (borrow @ [archive.org](https://archive.org/details/isbn_9781107439955)) ### Python * Python Scripting for Computational Science (borrow @ [archive.org](https://archive.org/details/pythonscriptingf0000lang)) ### Reactive Systems * A Practical Introduction To Real-Time Systems For Undergraduate Engineering (online @ [archive.org](https://archive.org/details/real-time_systems)) ### Refinement Calculus * a Practical Theory of Programming (online @ [www.cs.toronto.edu](https://www.cs.toronto.edu/~hehner/aPToP/)) * Refinement Calculus: A Systematic Introduction (online @ [lara.epfl.ch](https://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf)) ### Theorem Proving * Hyperproof (borrow @ [archive.org](https://archive.org/details/hyperproof0000barw)) ### Theory of Computation * Theory of Recursive Functions and Effective Computability (borrow @ [archive.org](https://archive.org/details/theoryofrecursiv00roge)) * Computability Theory, Semantics, and Logic Programming (borrow @ [archive.org](https://archive.org/details/computabilitythe0000fitt)) ### Type Theory * Basic Simple Type Theory (borrow with print disabilities @ [archive.org](https://archive.org/details/basicsimpletypet0000hind)) * Type Theory and Functional Programming (online @ [www.cs.kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf)) * Programming in Martin-Löf’s Type Theory (online @ [www.cse.chalmers.se](http://www.cse.chalmers.se/research/group/logic/book/)) ### x86 * 80286 Assembly Language on MS-DOS Computers (borrow @ [archive.org](https://archive.org/details/80286assemblylan00scan)) * 80386 -- A Programming and Design Handbook (borrow @ [archive.org](https://archive.org/details/80386aprogrammin0000brum)) * The x86 PC (borrow @ [archive.org](https://archive.org/details/x86pcassemblylan0005mazi)) * IA-64 for Software Developers (borrow @ [archive.org](https://archive.org/details/ia64architecture0000trie)) * PC Assembly Book (online @ [pacman128.github.io](https://pacman128.github.io/pcasm/)) Unrated Papers -------------- ### Abstract Algebra * [The Convolution Algebra](https://math.nmsu.edu/people/personal-pages/files/2018-The-Convolution-Algebra.pdf) * [Algebras and combinators](https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/68681/eth-3148-01.pdf) * [Algebras and combinators (Algebra universalis 1981)](https://people.math.ethz.ch/~engeler/g_AlgebrasAndCombinators.pdf) * [Equations in Combinatory Algebras](https://people.math.ethz.ch/~engeler/Engeler1984_Chapter_EquationsInCombinatoryAlgebras.pdf) * [Higher-Order Algebraic Theories](https://www.cl.cam.ac.uk/~na412/Higher-order%20algebraic%20theories.pdf) ### Category Theory * Physics, Topology, Logic and Computation: A Rosetta Stone (online @ [arxiv.org](https://archive.org/details/arxiv-0903.0340)) ### Computational Complexity * Complexity Hierarchies Beyond Elementary (online @ [arxiv.org](https://arxiv.org/abs/1312.5686)) * Pure vs Impure Lisp (online @ [dl.acm.org](https://dl.acm.org/doi/pdf/10.1145/244795.244798)) ### Coq * Recursive Datatypes and Inductive Proofs (online @ [www.inf.ed.ac.uk](https://www.inf.ed.ac.uk/teaching/courses/ar/slides/lec14/Coq_Induction.pdf)) * Interactive Theorem Proving with Coq (online @ [people.eecs.berkeley.edu](https://people.eecs.berkeley.edu/~necula/autded/lecture18-coq.pdf)) ### Equational Logic * [Second-Order Equational Logic](https://www.cl.cam.ac.uk/~mpf23/papers/Types/soeqlog.pdf) ### Formal Specification * [Consistency Checking of Functional Requirements](https://arxiv.org/abs/1804.10486) * [Consistency Checking in Requirements Analysis](https://jar-ben.github.io/papers/ISSTA2017.pdf) * [Automated Consistency Checking of Requirements Specifications](https://apps.dtic.mil/sti/tr/pdf/ADA465574.pdf) ### Functional Programming * let (rec) insertion without effects, lights or magic (online @ [icfp19.sigplan.org](https://icfp19.sigplan.org/details/mlfamilyworkshop-2019-papers/6/let-rec-insertion-without-effects-lights-or-magic)) ### Incompleteness * A Simple Character String Proof of the \"True but Unprovable\" Version of Goedel\'s First Incompleteness Theorem (online @ [arxiv.org](https://arxiv.org/abs/1402.7253)) * A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points (online @ [arxiv.org](https://arxiv.org/abs/math/0305282)) * Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles (online @ [jstor](https://www.jstor.org/stable/2695030)) ### Macros * Hygiene for the Unhygienic (online @ [www.p-cos.net](http://www.p-cos.net/documents/hygiene.pdf), [guenchi.github.io](https://guenchi.github.io/Scheme/doc/Hygiene-Compatible%20Macros%20in%20an%20Unhygienic%20Macro%20System.pdf)) * [Binding as Sets of Scopes](https://www.cs.utah.edu/plt/scope-sets/) ### Modal Logic * Modal Mu-Calculi (online @ [www.julianbradfield.org](https://www.julianbradfield.org/Research/MLH-bradstir.pdf)) ### Name Binding * [A Type and Scope Safe Universe of Syntaxes with Binding](https://pure.strath.ac.uk/ws/portalfiles/portal/114903157/Allais_etal_ICFP2018_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf) * [Don’t Substitute Into Abstractions (Functional Pearl)](https://benl.ouroborus.net/papers/2016-dsim/lambda-dsim-20160328.pdf) * [Viewing λ-terms through Maps](https://www.mathematik.uni-muenchen.de/~schwicht/papers/lambda13/lamtheory8.pdf) * [A nominal axiomatisation of the lambda-calculus](http://gabbay.org.uk/papers/nomalc.pdf) ### Public Domain * Abandoning Copyright (online @ [papers.ssrn.com](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3543654)) ### Refinement Calculus * [Program Derivation by Correctness Enhancements](https://arxiv.org/abs/1606.02020) ### Relational Programming * [Relational programming](https://archive.org/details/relationalprogra83012macl) ### Term Rewriting * [The Rho Cube](https://link.springer.com/content/pdf/10.1007/3-540-45315-6_11.pdf) ### Theorem Proving * From LCF to HOL (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf)) * Towards self-verification of HOL Light (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf)) * A Self-Verifying Theorem Prover (online @ [www.kookamara.com](https://www.kookamara.com/jared/dissertation.pdf)) ### Theory of Computation * Unpredictability and Undecidability in Dynamical Systems (online @ [gwern.net](https://gwern.net/doc/cs/computable/1990-moore.pdf), [scribd.com](https://www.scribd.com/doc/2626932/Unpredictability-and-undecidability-in-dynamical-systems)) * Decidability and Undecidability in Dynamical Systems (online @ [inria.hal.science](https://inria.hal.science/inria-00429965v1/document)) ### Type Theory * Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega (online @ [web.cs.ucla.edu](https://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf))