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.
- Jeremy Avigad, "Mathematics and language," pdf
- Kenneth Manders, "Expressive means and mathematical understanding," pdf
- Jeremy Avigad, "Mathematical method and proof"
- 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.
- 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.
- 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.
- 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.
- 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.
- Steve Awodey, "Structure in Mathematics and Logic: A Categorical Perspective"
- Barr and Wells, Toposes, triples, and theories