Reading List

Table of Contents

This page was an experiment in recording a lit of the things I was reading. I didn’t not keep the listing up. As I am not at al sure of its value.

I began recording on (since <2018-04-08 Sun>), and the record keeping was spotty and inaccurate, since it also included things I inteded to read in coming months and years (and years)1.

Currently Reading

Modules for Standard ML

Type theory and formal proof: an introduction

Have Read

Texts in this list are read to my satisfaction for the moment. They are liable to move back to one of the other lists.


Bidirectional typing rules: a tutorial (2013).

1ML: Core and Modules United

<2019-09-20 Fri> (ref: ROSSBERG_2018)

Analytic and Synthetic Judgements in Type Theory

<2019-08-14 Wed> Martin_L_f_1994

An Introduction to Mathematics

<2019-09-23 Mon>

(ref: whitehead93)


The Purely Functional Software Deployment Model

<2019-02-01 Fri>

(ref: DBLP:phd/basesearch/Dolstra06)

Constructive Mathematics and Computer Programming

<2019-01-13 Sun>

(ref: Martin_L_f_1982)

On the semantics of lazy evaluation

The term lazy has is appropriate because only as few computation steps are made as are absolutely necessary to bring an expression into canonical form. However, what turns out to be of no significance, it is no longer the case that an expressions cannot have a value unless all its parts have values. For example, a' has itself as value even if a has no value. What is significant, though, is that the principle of Frege’s referred to earlier, namely that the value of an expression depends only on the values of its parts, is irretrievably lost. To make the language work in spite of this loss has been one of the most serious difficulties in the design of the theory of types. (172)

From the discussion notes after the chapter

… if propositions were interpreted as domains and truth as non-emptiness, every proposition would come out true. This is why I could not think of dealing with partial elements and functions, that is, possibly non-terminating programs, before I had freed myself from the interpretation of propositions as types. (184)


Build systems a la carte

<2018-11-15 Thu>

(ref Mokhov_2018)

Networks: A Very Short Introduction

<2018-08-13 Mon>

(ref: caldarelli2012networks)

“Marx’s Concept Of Socialism” from Eric Fromm’s Marx’s Concept of Man

<2018-08-09 Thu>

Marx expressed the aim of socialism with great clarity at the end of the third volume of Capital: “In fact, the realm of freedom does not commence until the point is passed where labor under the compulsion of necessity and of external utility is required. In the very nature of things it lies beyond the sphere of material production in the strict meaning of the term. Just as the savage must wrestle with nature, in order to satisfy his wants, in order to maintain his life and reproduce it, so civilized man has to do it, and he must do it in all forms of society and under all possible modes of production. With his development the realm of natural necessity expands, because his wants increase; but at the same time the forces of production increase, by which these wants are satisfied. The freedom in this field cannot consist of anything else but of the fact that socialized man, the associated producers, regulate their interchange with nature rationally, bring it under their common control, instead of being ruled by it as by some blind power; they accomplish their task with the least expenditure of energy and under conditions most adequate to their human nature and most worthy of it. But it always remains a realm of necessity. Beyond it begins that development of human power, which is its own end, the true realm of freedom, which, however, can flourish only upon that realm of necessity as its basis.”

The Triumph of Types: Principia Mathematica’s Impact on Computer Science

(ref: ConstableManuscript-CONTTO-4)

<2018-08-07 Tue>

2.5 Effectively Computable, Turing Computable, and Subrecur-sive Computation

Systems Brouwer’s notion of computability is not formal and not axiomatic. It is intuitive and corresponds to what is called effective computability . The Church/Turing Thesis claims that all effectively computable functions are computable by Turing machines (or any equivalent formalism, e.g. the untyped λ -calculus). There is no corresponding formalism for Brouwer Computable . However, I believe that this notion can be captured in intuitionistic logics by leaving a Turing complete computation system for the logic open-ended in the sense that new primitive terms and rules of reduction are possible. This method of capturing effective computability may be unique to CTT in the sense that the computation system of CTT is open to being “Brouwer complete” as a logic. We have recently added a primitive notion of general process to formalize distributed systems whose potentially nonterminating computations are not entirely deterministic because they depend on asynchronous message passing over a network which can only be modeled faithfully by allowing

Structuralism, Invariance, and Univalence

(ref: Awodey_2013)

<2018-07-26 Thu>

Frob: Functional Reactive Programming Applied to Robotics

(ref: hagerfrob)

<2018-07-20 Fri>

Community, Democracy, and Mutual Aid

(ref: Colon_2017)

<2018-07-05 Thu>

Articulates an inspiring philosophy, vision, and strategy for pursuing radically democratic, cooperative, solidarity-based dual power institutions to undermine (and hopefully replace) the exploitative and oppressive systems we inhabit.

Feel the Heat: An Embodied Approach to the Instruction of the Greenhouse Effect

By Ian Thacker (Not yet published)

<2018-04-27 Fri>

Motto: “Perceptual inferences become causal rules”

Consistent Overhead Byte Stuffing

(ref: cheshire1999consistent)

<2018-04-24 Tue>

A Theory of the Learnable

(ref: valiant84_theor_learn)

<2018-04-18 Wed>


The Marx and Engels Reader

Chapters read
  • “Marx on the History of his Opinions”
  • “Discovering Hegel”
  • “To Make the World Philosophical”
  • “For a Ruthless Criticism of Everything Existing”

The Inoperative Community

Chapters read
  • “The Inoperative Community”
  • “Literary Communism”

Want to Read

Texts in this list are not being actively read, but they may have been started or partially read. They are, in any case, yet to be completed.

On the Meanings of the Logical Constants and the Justifications of the Logical Laws

Intuitionistic Type Theory

Miscomputation in Software: Learning to live with errors

(ref: Petricek_2017)

Logic -> TypeTheory+

Listed in approximate order of ascent.

Software Foundations: Logical Foundations

(ref: Pierce:SF)


On Axiomatic Systems for Arbitrary Systems of Sentences

Investigations into Logical Deduction

Natural Deduction

(ref: dag06_natur)

Type Theory and Formal Proof

(ref: rob2014type)

(Abstract) Algebra -> Topology+

Listed in approximate order of ascent.

Experiments in Topology

(ref: barr89_exper)

Conceptual Mathematics

(ref: f.08_concep)


Topoi: the Categorial Analysis of Logic

The Blind Spot

(ref: girard11)




This list is not complete. It only reflects writing which I remembered to enter and which I felt were actually worth the time to enter.


  • [macqueen84_modul_ml] David MacQueen, Modules for standard ML, nil, in in: Proceedings of the 1984 ACM Symposium on LISP and functional programming - LFP '84, edited by (1984)
  • [rob2014type] Rob Nederpelt & Geuvers, Type Theory and Formal Proof: An Introduction, Cambridge University Press (2014).
  • [christiansen2013bidirectional] @miscchristiansen2013bidirectional, title = Bidirectional Typing Rules: A Tutorial, author = Christiansen, David Raymond, year = 2013
  • [ROSSBERG_2018] ROSSBERG, 1ML – Core and modules united, Journal of Functional Programming, 28, (2018). link. doi.
  • [Martin_L_f_1994] Martin-Löf, Analytic and Synthetic Judgements in Type Theory, Kant and Contemporary Epistemology, 87–99 (1994). link. doi.
  • [whitehead93] Alfred North Whitehead, An introduction to mathematics, Oxford University Press (1993).
  • [DBLP:phd/basesearch/Dolstra06] @phdthesisDBLP:phd/basesearch/Dolstra06, author = Eelco Dolstra, title = The purely functional software deployment model, school = Utrecht University, Netherlands, year = 2006, url =, timestamp = Tue, 21 Mar 2017 00:00:00 +0100, biburl =, bibsource = dblp computer science bibliography,
  • [Martin_L_f_1982] Martin-Löf, Constructive Mathematics and Computer Programming, Studies in Logic and the Foundations of Mathematics, 153–175 (1982). link. doi.
  • [Mokhov_2018] Mokhov, Mitchell & Peyton Jones, Build systems à la carte, Proceedings of the ACM on Programming Languages, 2(ICFP), 1–29 (2018). link. doi.
  • [caldarelli2012networks] Caldarelli & Catanzaro, Networks: A Very Short Introduction, OUP Oxford (2012).
  • [ConstableManuscript-CONTTO-4] @unpublishedConstableManuscript-CONTTO-4, author = Robert L. Constable, title = The Triumph of Types: Principia Mathematica's Impact on Computer Science
  • [Awodey_2013] Awodey, Structuralism, Invariance, and Univalence, Philosophia Mathematica, 22(1), 1–11 (2013). link. doi.
  • [hagerfrob] Hager, Peterson & Nilsson, Frob: Functional Reactive Programming Applied to Robotics, , .
  • [Colon_2017] Colón, Herson-Hord, Horvath, , Martindale & Porges, Community, Democracy, and Mutual Aid: Toward Dual Power and Beyond, Next System Project National Essay Competition, (2017).
  • [cheshire1999consistent] Cheshire & Baker, Consistent overhead byte stuffing, IEEE/ACM Transactions on networking, 7(2), 159-172 (1999).
  • [valiant84_theor_learn] Valiant, A Theory of the Learnable, Communications of the ACM, 27(11), 1134-1142 (1984). link. doi.
  • [tucker78_marx_engel] Robert Tucker, The Marx-Engels reader, Norton (1978).
  • [peter01] Jean-Luc Nancy; by Peter Connor, The inoperative community, University of Minnesota Press (2001).
  • [Martin-Lof1996-MAROTM-7] Per Martin-L\"of, On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic Journal of Philosophical Logic, 1(1), 11-60 (1996).
  • [martin1984intuitionistic] Martin-L\"of & Sambin, Intuitionistic type theory, Bibliopolis Napoli (1984).
  • [Petricek_2017] Petricek, Miscomputation in software: Learning to live with errors, The Art, Science, and Engineering of Programming, 1(2), (2017). link. doi.
  • [Pierce:SF] Benjamin Pierce, Arthur Azevedo de Amorim, Chris, Casinghino, Marco Gaboardi, Michael Greenberg, , C\vat\valin Hri\ctcu, Vilhelm Sj\"oberg, Brent & Yorgey, Software Foundations, Electronic textbook (2017).
  • [hertz12_axiom_system_arbit_system_senten] @inbookhertz12_axiom_system_arbit_system_senten, date_added = Sat Mar 12 21:09:54 2016, author = Paul Hertz and Javier Legris, booktitle = Universal Logic: An Anthology, doi = 10.1007/978-3-0346-0145-0_2, pages = 11-29, publisher = Springer Science + Business Media, series = Universal Logic: An Anthology, title = On Axiomatic Systems for Arbitrary Systems of Sentences, url =, year = 2012,
  • [m.69_gerhar_gentz_german] edited by Szabo, The collected papers of Gerhard Gentzen / (translated from the German)., North-Holland Publishing (1969).
  • [dag06_natur] Dag Prawitz, Natural deduction a proof-theoretical study, Dover publications (2006).
  • [barr89_exper] Stephen Barr, Experiments in topology, Dover Publications (1989).
  • [f.08_concep] William Lawvere, Conceptual mathematics : a first introduction to categories, Cambridge University Press (2008).
  • [saunders88_algeb] Saunders MacLane, Algebra, Chelsea Pub. Co. (1988).
  • [robert06_topoi] Robert Goldblatt, Topoi : the categorial analysis of logic, Dover Publications (2006).
  • [girard11] Jean-Yves Girard, The blind spot : lectures on logic, European Mathematical Society (2011).