Unrated Resources ================= Unrated Webpages -------------- ### Systems Theory * [Leverage Points: Places to Intervene in a System - The Donella Meadows Project](https://donellameadows.org/archives/leverage-points-places-to-intervene-in-a-system/) * [How Complex Systems Fail](https://how.complexsystems.fail/) * [LOOPY: a tool for thinking in systems](https://ncase.me/loopy/) Unrated Books -------------- ### Agile Development * Agile Systems Engineering (borrow @ [archive.org](https://archive.org/details/agilesystemsengi0000doug)) ### Artificial Intelligence * Building Problem Solvers (borrow @ [archive.org](https://archive.org/details/buildingproblems0000forb)) ### 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)) ### Chaos Theory * Chaos: Making a New Science (borrow @ [archive.org](https://archive.org/details/chaosmakingnewsc0000unse)) ### Computational Complexity * Computational Complexity (Wagner and Wechsung) (borrow @ [archive.org](https://archive.org/details/computationalcom0000wagn)) ### 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)) ### 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)) * Mr Pye (borrow @ [archive.org](https://archive.org/details/mrpye0000peak_a2p9)) ### 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)) * Handbook of Logic in Computer Science, Volume 1 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0001unse_z8j4)) * Handbook of Logic and Proof Techniques for Computer Science (borrow @ [archive.org](https://archive.org/details/handbookoflogicp0000kran)) * Handbook of logic in artificial intelligence and logic programming, Vol 1 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0001unse)) * Handbook of logic in artificial intelligence and logic programming, Vol 2 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0002unse)) * Handbook of logic in artificial intelligence and logic programming, Vol 4 (borrow @ [archive.org](https://archive.org/details/handbookoflogici0004unse)) ### Logic Programming * Programming with Higher-Order Logic (borrow @ [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)) ### PLDI * Threaded Interpretive Languages (online @ [archive.org](https://archive.org/details/R.G.LoeligerThreadedInterpretiveLanguagesTheirDesignAndImplementationByteBooks1981)) ### Partial Evaluation * Partial Evaluation and Automatic Program Generation (online @ [www.itu.dk](http://www.itu.dk/people/sestoft/pebook/)) ### Proof Theory * Basic Proof Theory (borrow @ [archive.org](https://archive.org/details/basicprooftheory0000troe)) ### 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)) ### 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 @ [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 * 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) ### 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)) ### 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)) ### Lambda Calculus * [On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control](https://members.loria.fr/PdeGroote/papers/lpar94.pdf) ### 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) ### 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)) ### 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)) Unrated Repositories --------------