Bibliography

These are some works relevant to the topic of the seminar. I have been lazy about bibliographical details, but Google will supply these. To avoid copyright violations, some of the links are to copies kept in a password-protected directory. This list will evolve and grow over the course of the semester.

General considerations

• Jeremy Avigad, "Mathematics and language," pdf
• Kenneth Manders, "Expressive means and mathematical understanding," pdf
• Jeremy Avigad, "Mathematical method and proof" doi, pdf.
• Yacin Hamami, "Mathematical rigor, proof gap, and the validity of mathematical inference," pdf
• Mahi Hardalupas, "When is a proof not a proof?: A computer-aided evaluation of the mathematical notion of proof," pdf

Interactive theorem proving: overviews

• Jeremy Avigad and John Harrison, "Formally verified mathematics," pdf.
• Thomas C. Hales, "Developments in formal proofs," pdf.
• Thomas C. Hales, "Mathematics in the age of the Turing machine," arXiv.
• Jeremy Avigad, Review of Hales, Dense Sphere Packings: A Blueprint for Formal Proofs, pdf.
• Jesse Alama and Reinhard Kahle, "Checking proofs," pdf.
• Jesse Alama and Reinhard Kahle, "Computing with Mathematical Arguments," publisher.
• Notices of the AMS, Special Issue on Formal Proof, with contributions by Thomas Hales, Georges Gonthier, John Harrison, and Freek Wiedijk, pdf.
• Jeremy Avigad, "Understanding, formal verification, and the philosophy of mathematics," pdf.

Interactive theorem provers: languages

• de Bruijn, "The mathematical vernacular: a language for mathematics with typed sets," pdf.
• Freek Wiedijk, "The mathematical vernacular," pdf.
• Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz, "Mizar in a Nutshell," journal.
• Georges Gonthier, Assia Mahboubi, and Enrico Tassi, "A Small Scale Reflection Extension for the Coq System," pdf.
• Tobias Nipkow, Lawrence Paulson, and Makarius Wenzel, Isabelle HOL: A Proof Assistant for Higher-Order Logic, pdf.
• Tobias Nipkow, Programming and Proving in Isabelle/HOL, pdf.
• Jeremy Avigad, Leonardo de Moura, and Soonho Kong, Theorem Proving in Lean, pdf.
• Frank Pfenning, "Logical frameworks: a brief introduction," pdf.

Interactive theorem provers: formalizations

• Tom Hales et al., "A formal proof of the Kepler Conjecture," pdf.
• Georges Gonthier et al., "A machine checked proof of the odd order theorem", pdf.
• John Harrison, "A formal proof of Pick's theorem," pdf.
• Johannes Hölzl, Fabian Immler, and Brian Huffman, "Type Classes and Filters for Mathematical Analysis in Isabelle/HOL", pdf.

Formal models of mathematical language

• Mohan Ganesalingam, "The language of mathematics," html.
• Andrei Paskevich, "The syntax and semantics of the ForTheL language," pdf.
• The Naproche project, html.
• Jeremy Avigad, "Type inference in mathematics," pdf.
• George Boolos, "Don't eliminate cut"
• George Boolos, "A curious inference"

Philosophy of language and linguistics

• Ludwig Wittgenstein, Philosophical investigations.
• Richard Rorty, ed., The Linguistic Turn: Recent Essays in Philosophical Method.
• Rudolf Carnap, "Empiricism, semantics, and ontology," pdf.
• James W. Cornman, "Language and ontology," pdf.
• Willard v.O. Quine, "Semantic ascent" (excerpt from Word and Object), pdf.
• David Kaplan, "The meaning of ouch and oops," pdf, pdf transcript of talk, youtube.
• Gregory Ward and Betty J. Birner, "Discourse effects of word order variation," pdf.
• Some examples of mathematical language: Hatcher, pdf, Hardy and Wright, pdf, pdf
• Paul Bloom and Frank C. Keil, "Thinking through language," pdf.

Designed languages

• Arika Okrent, In the Land of Invented Languages: Esperanto Rock Stars, Klingon Poets, Loglan Lovers and the Mad Dreamers who tried to Build a Perfect Language
• Umberto Eco, The Search for the Perfect Language
• John Wilkins, An Essay Towards a Real Character and a Philosophical Language, Google Books
• George Dalgarno, The works of George Dalgarno, Google Books.
• Jorge Luis Borges, "The analytical language of John Wilkins," html
• Jaap Maat, Philosophical Languages in the Seventeenth Century
• Rudolf Carnap, "The problem of a world language," pdf
• James Cooke Brown, "Loglan" (from Scientific American), pdf.
• James Cooke Brown, Loglan 1: A Logical Language
• Arnold M. Zwicky, Review of Loglan: A Logical Language, pdf.
• The Lojban weg page (try the lightning talk), html.

Modularity

• Herbert A. Simon, "The architecture of complexity," pdf.
• Herbert A. Simon, The sciences of the artificial
• Carliss Y. Baldwin and Kim B. Clark, Design Rules, Volume 1: The Power of Modularity
• H. Clark Barrett and Robery Kurzan, "Modularity in Cognition: Framing the Debate," pdf.
• David L. Parnas, "On the Criteria to Be Used in Decomposing systems into Modules," pdf.

Programming methodology

• Harold Abelson, Gerald Jay Sussman, and Julie Sussman, Structure and Interpretation of Computer Programs, pdf.
• Martin Fowler, Refactoring: Improving the Design of Existing Code

Programming language design

• John Reynolds, "Types, abstraction, and parametric polymorphism," pdf.
• Robert Harper, Practical Foundations for Programming Languages, pdf.
• Benjamin Pierce, Types and Programming Languages
• Walter Bright, "So you want to design your own language?" pdf.
• Paul Graham, "Five questions about language design," html.
• Andrej Bauer, "On programming language design," html.
• "PHP: a fractal of bad design," html

Insights from the history of mathematics

• Ken Manders, "Euclid or Descartes: representation and responsiveness"
• Jeremy Avigad and Rebecca Morris, "The concept of 'character' in Dirichlet's theorem on primes in an arithmetic progression," arXiv, or doi.
• Jeremy Avigad and Rebecca Morris, "Character and object," pdf.

Automated reasoning

• John Harrison, Handbook of practical logic and automated reasoning.
• J. Alan Robinson and Andrei Voronkov, editors, Handbook of automated reasoning, volumes 1 and 2.

Philosophy of mathmatical practice

• Jamie Tappenden, "Proof style and understanding in mathematics I: visualization, unification and axiom choice," pdf.
• Johannes Hafner and Paolo Mancosu, "The varieties of mathematical explanation"
• Paolo Mancosu, "Mathematical explanation: why it matters," pdf.
• Paolo Mancosu, "Mathematical style," SEP.
• Paolo Mancosu, "Explanation in mathematics," SEP.
• Andrew Arana, "Logical and semantic purity," pdf.
• Michael Detlefsen, "Purity as an ideal of proof," pdf.
• Andrew Arana and Michael Detlefsen, "Purity of methods," pdf.
• Michael Detlefsen, "Duality, epistemic efficiency and consistency," pdf
• Andrew Arana, "On the depth of Szemeredi's theorem," pdf.
• Rebecca Morris, Appropriate steps: a theory of motivated proof, pdf.

Categorical language

• Steve Awodey, "Structure in Mathematics and Logic: A Categorical Perspective"
• Barr and Wells, Toposes, triples, and theories