# Reading List

## Table of Contents

- Currently Reading
- Have Read
- 2019
- 2018
- Build systems a la carte
- Networks: A Very Short Introduction
- “Marx’s Concept Of Socialism” from Eric Fromm’s
*Marx’s Concept of Man* - The Triumph of Types: Principia Mathematica’s Impact on Computer Science
- Structuralism, Invariance, and Univalence
- Frob: Functional Reactive Programming Applied to Robotics
- Community, Democracy, and Mutual Aid
- Feel the Heat: An Embodied Approach to the Instruction of the Greenhouse Effect
- Consistent Overhead Byte Stuffing
- A Theory of the Learnable
- The Marx and Engels Reader
- The Inoperative Community

- Want to Read

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 ^{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.

### 2019

#### Bidirectional typing rules: a tutorial (2013).

#### 1ML: Core and Modules United

#### Analytic and Synthetic Judgements in Type Theory

#### An Introduction to Mathematics

#### The Purely Functional Software Deployment Model

#### Constructive Mathematics and Computer Programming

(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)

### 2018

#### Build systems a la carte

(ref Mokhov_2018)

#### Networks: A Very Short Introduction

(ref: caldarelli2012networks)

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

https://www.marxists.org/archive/fromm/works/1961/man/ch06.htm

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)

2.5 Effectively Computable, Turing Computable, and Subrecur-sive ComputationSystems 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)

#### Frob: Functional Reactive Programming Applied to Robotics

(ref: hagerfrob)

#### Community, Democracy, and Mutual Aid

(ref: Colon_2017)

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)

Motto: “Perceptual inferences become causal rules”

#### Consistent Overhead Byte Stuffing

(ref: cheshire1999consistent)

#### A Theory of the Learnable

#### 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”

## 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

(ref: Martin-Lof1996-MAROTM-7)

### Intuitionistic Type Theory

(ref: martin1984intuitionistic)

### Miscomputation in Software: Learning to live with errors

(ref: Petricek_2017)

### Logic -> TypeTheory+

Listed in approximate order of ascent.

#### On Axiomatic Systems for Arbitrary Systems of Sentences

#### Investigations into Logical Deduction

(ref: m.69_gerhar_gentz_german)

#### 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)

#### Algebra

(ref: saunders88_algeb)

#### Topoi: the Categorial Analysis of Logic

(ref: robert06_topoi)

## Footnotes:

^{1}

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.

# Bibliography

- [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 = http://dspace.library.uu.nl:8080/handle/1874/7540, timestamp = Tue, 21 Mar 2017 00:00:00 +0100, biburl = https://dblp.org/rec/bib/phd/basesearch/Dolstra06, bibsource = dblp computer science bibliography, https://dblp.org
- [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 = http://dx.doi.org/10.1007/978-3-0346-0145-0_2, 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).