|
| 1 | +<!DOCTYPE html> |
| 2 | +<!-- Academia (pandoc HTML5 template) |
| 3 | + designer: soimort |
| 4 | + last updated: 2016-05-07 --> |
| 5 | +<html> |
| 6 | + <head> |
| 7 | + <meta charset="utf-8"> |
| 8 | + <meta name="generator" content="pandoc"> |
| 9 | + <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes"> |
| 10 | + <title>Programming Languages</title> |
| 11 | + <link rel="canonical" href="https://wiki.soimort.org/plt"> |
| 12 | + <style type="text/css">code { white-space: pre; }</style> |
| 13 | + <link rel="stylesheet" href="//cdn.soimort.org/normalize/4.1.1/normalize.min.css"> |
| 14 | + <link rel="stylesheet" href="//cdn.soimort.org/mathsvg/latest/mathsvg.min.css"> |
| 15 | + <link rel="stylesheet" href="//cdn.soimort.org/fonts/api/Latin-Modern-Roman.css"> |
| 16 | + <link rel="stylesheet" href="//cdn.soimort.org/fonts/api/Latin-Modern-Mono.css"> |
| 17 | + <link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/font-awesome/4.6.3/css/font-awesome.min.css"> |
| 18 | + <link rel="stylesheet" href="/__/css/style.css"> |
| 19 | + <!--[if lt IE 9]> |
| 20 | + <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script> |
| 21 | + <![endif]--> |
| 22 | + <script src="//cdn.soimort.org/jk/latest/jk.min.js"></script> |
| 23 | + <script src="//cdn.soimort.org/mathsvg/latest/mathsvg.min.js"></script> |
| 24 | + <script src="/__/js/jk-minibar.js"></script> |
| 25 | + <link rel="icon" href="/favicon.png"> |
| 26 | + <link rel="apple-touch-icon" href="/favicon.png"> |
| 27 | + </head> |
| 28 | + <body> |
| 29 | + <main><article> |
| 30 | + <header> |
| 31 | + <h1 class="title">Programming Languages</h1> |
| 32 | + <h1 class="subtitle">Reading List (Temporary)</h1> |
| 33 | + </header> |
| 34 | + <nav id="TOC"> |
| 35 | +<ul> |
| 36 | +<li><a href="#functional-programming">Functional Programming</a></li> |
| 37 | +<li><a href="#programming-paradigms">Programming Paradigms</a></li> |
| 38 | +<li><a href="#programming-languages">Programming Languages</a></li> |
| 39 | +<li><a href="#abstract-algebra">Abstract Algebra</a><ul> |
| 40 | +<li><a href="#category-theory">Category Theory</a></li> |
| 41 | +</ul></li> |
| 42 | +<li><a href="#mathematical-logic-and-foundations-of-mathematics">Mathematical Logic and Foundations of Mathematics</a></li> |
| 43 | +<li><a href="#lambda-calculus">Lambda Calculus</a></li> |
| 44 | +<li><a href="#type-theory">Type Theory</a></li> |
| 45 | +<li><a href="#compiler-construction">Compiler Construction</a></li> |
| 46 | +</ul> |
| 47 | + </nav> |
| 48 | + <div id="content"> |
| 49 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Programming_language_theory">Programming language theory</a>]</p> |
| 50 | +<section id="functional-programming" class="level2"> |
| 51 | +<h2>Functional Programming</h2> |
| 52 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Functional_programming">Functional programming</a>]</p> |
| 53 | +<p>Books:</p> |
| 54 | +<ul> |
| 55 | +<li><em>How to Design Programs</em> (<strong>HtDP</strong>) (by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi) [<a href="http://htdp.org/">Homepage</a>] [<a href="http://htdp.org/2003-09-26/Book/">HTML</a>] [<a href="http://www.ccs.neu.edu/home/matthias/HtDP2e/">HTML</a> (2nd Ed.)]</li> |
| 56 | +<li><em>Structure and Interpretation of Computer Programs</em> (<strong>SICP</strong>, <strong>“Wizard Book”</strong>) (by Gerald Jay Sussman, Hal Abelson, Julie Sussman) [<a href="http://mitpress.mit.edu/sicp/">Homepage</a>] [<a href="http://mitpress.mit.edu/sicp/full-text/book/book.html">HTML</a>] [<a href="https://github.com/sarabander/sicp-pdf/blob/master/sicp.pdf?raw=true">PDF</a> (Unofficial)]</li> |
| 57 | +<li><em>Introduction to Functional Programming</em> (by Richard Bird, Philip Wadler) [<a href="http://www.nlda-tw.nl/janmartin/vakken/TFIT/Extra%20materiaal/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf">PDF</a>]</li> |
| 58 | +<li><em>Pearls of Functional Algorithm Design</em> (by Richard Bird)</li> |
| 59 | +<li><em>Purely Functional Data Structures</em> (by Chris Okasaki) [<a href="http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf">PDF</a>] |
| 60 | +<ul> |
| 61 | +<li>StackExchange: <em>What’s new in purely functional data structures since Okasaki?</em> [<a href="http://cstheory.stackexchange.com/questions/1539/whats-new-in-purely-functional-data-structures-since-okasaki">Link</a>]</li> |
| 62 | +</ul></li> |
| 63 | +</ul> |
| 64 | +</section> |
| 65 | +<section id="programming-paradigms" class="level2"> |
| 66 | +<h2>Programming Paradigms</h2> |
| 67 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Programming_paradigm">Programming paradigm</a>]</p> |
| 68 | +<p>Books:</p> |
| 69 | +<ul> |
| 70 | +<li><em>Concepts, Techniques, and Models of Computer Programming</em> (<strong>CTM</strong>, <strong>“Oz Book”</strong>) (by Peter Van Roy, Seif Haridi) [<a href="http://www.info.ucl.ac.be/~pvr/book.html">Homepage</a>]</li> |
| 71 | +</ul> |
| 72 | +</section> |
| 73 | +<section id="programming-languages" class="level2"> |
| 74 | +<h2>Programming Languages</h2> |
| 75 | +<p>Books:</p> |
| 76 | +<ul> |
| 77 | +<li><em>Essentials of Programming Languages</em> (<strong>EOPL</strong>) (by Daniel P. Friedman, Mitchell Wand, Christopher T. Haynes) [<a href="http://www.eopl3.com/">Homepage</a>] [<a href="https://github.com/mwand/eopl3">Code</a>]</li> |
| 78 | +<li><em>Programming Languages: Application and Interpretation</em> (<strong>PLAI</strong>) (by Shriram Krishnamurthi) [<a href="http://cs.brown.edu/~sk/Publications/Books/ProgLangs/">Homepage</a>] [<a href="http://cs.brown.edu/courses/cs173/2012/book/">HTML</a>] [<a href="http://www.cs.brown.edu/courses/cs173/2012/book/book.pdf">PDF</a>]</li> |
| 79 | +</ul> |
| 80 | +</section> |
| 81 | +<section id="abstract-algebra" class="level2"> |
| 82 | +<h2>Abstract Algebra</h2> |
| 83 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Abstract_algebra">Abstract algebra</a>]</p> |
| 84 | +<p>Online resources:</p> |
| 85 | +<ul> |
| 86 | +<li>Wikibooks: <em>Abstract Algebra</em> [<a href="https://en.wikibooks.org/wiki/Abstract_Algebra">HTML</a>]</li> |
| 87 | +</ul> |
| 88 | +<p>Books:</p> |
| 89 | +<ul> |
| 90 | +<li><em>A Book of Abstract Algebra</em> (by Charles C. Pinter)</li> |
| 91 | +</ul> |
| 92 | +<section id="category-theory" class="level3"> |
| 93 | +<h3>Category Theory</h3> |
| 94 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Category_theory">Category theory</a>]</p> |
| 95 | +<p>Books:</p> |
| 96 | +<ul> |
| 97 | +<li><em>Category Theory for Computing Science</em> (<strong>CTCS</strong>) (by Michael Barr, Charles Wells) [<a href="http://www.tac.mta.ca/tac/reprints/articles/22/tr22abs.html">Homepage</a>] [<a href="http://www.tac.mta.ca/tac/reprints/articles/22/tr22.pdf">PDF</a>]</li> |
| 98 | +<li><em>Basic Category Theory for Computer Scientists</em> (by Benjamin C. Pierce)</li> |
| 99 | +<li><em>Category Theory for Scientists</em> (by David Spivak) [<a href="http://math.mit.edu/~dspivak/CT4S.pdf">PDF</a>] [<a href="http://math.mit.edu/~dspivak/teaching/sp13/">Course Homepage</a> (MIT 18-S996)]</li> |
| 100 | +<li><em>Conceptual Mathematics: A First Introduction to Categories</em> (by F. William Lawere, Stephen H. Schanuel)</li> |
| 101 | +<li><em>Categories for the Working Mathematician</em> (by Saunders Mac Lane)</li> |
| 102 | +</ul> |
| 103 | +</section> |
| 104 | +</section> |
| 105 | +<section id="mathematical-logic-and-foundations-of-mathematics" class="level2"> |
| 106 | +<h2>Mathematical Logic and Foundations of Mathematics</h2> |
| 107 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Mathematical_logic">Mathematical logic</a>] [Wikipedia: <a href="https://en.wikipedia.org/wiki/Foundations_of_mathematics">Foundations of mathematics</a>]</p> |
| 108 | +<p>Online resources:</p> |
| 109 | +<ul> |
| 110 | +<li>Wikibooks: <em>Logic for Computer Scientists</em> [<a href="https://en.wikibooks.org/wiki/Logic_for_Computer_Scientists">HTML</a>]</li> |
| 111 | +</ul> |
| 112 | +<p>Books:</p> |
| 113 | +<ul> |
| 114 | +<li><em>The Haskell Road to Logic, Maths and Programming</em> (<strong>HR</strong>) (by Kees Doets, Jan van Eijck) [<a href="http://homepages.cwi.nl/~jve/HR/">Homepage</a>]</li> |
| 115 | +<li><em>Introduction to Logic and to the Methodology of Deductive Sciences</em> (by Alfred Tarski)</li> |
| 116 | +<li><em>Mathematical Logic</em> (by Stephen Cole Kleene)</li> |
| 117 | +<li><em>Introduction to Metamathematics</em> (by Stephen Cole Kleene)</li> |
| 118 | +<li><em>The Foundations of Mathematics</em> (by Kenneth Kunen)</li> |
| 119 | +</ul> |
| 120 | +</section> |
| 121 | +<section id="lambda-calculus" class="level2"> |
| 122 | +<h2>Lambda Calculus</h2> |
| 123 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Lambda_calculus">Lambda calculus</a>]</p> |
| 124 | +<p>Books:</p> |
| 125 | +<ul> |
| 126 | +<li><em>An Introduction to Functional Programming Through Lambda Calculus</em> (by Greg Michaelson) [<a href="http://www.cs.rochester.edu/~brown/173/readings/LCBook.pdf">PDF</a>]</li> |
| 127 | +<li><em>An Introduction to Lambda Calculi for Computer Scientists</em> (by Chris Hankin)</li> |
| 128 | +<li><em>Introduction to Lambda Calculus</em> (by Henk Barendregt, Erik Barendsen) [<a href="http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf">PDF</a>]</li> |
| 129 | +<li><em>The Lambda Calculus, Its Syntax and Semantics</em> (by Henk Barendregt)</li> |
| 130 | +<li><em>Lambda Calculus with Types</em> (by Henk Barendregt, Wil Dekkers, Richard Statman)</li> |
| 131 | +</ul> |
| 132 | +</section> |
| 133 | +<section id="type-theory" class="level2"> |
| 134 | +<h2>Type Theory</h2> |
| 135 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Type_theory">Type theory</a>]</p> |
| 136 | +<p>Online resources:</p> |
| 137 | +<ul> |
| 138 | +<li><em>Software Foundations</em> (<strong>SF</strong>) (by Benjamin C. Pierce, etc.) [<a href="http://www.cis.upenn.edu/~bcpierce/sf/">HTML</a>]</li> |
| 139 | +</ul> |
| 140 | +<p>Books:</p> |
| 141 | +<ul> |
| 142 | +<li><em>Types and Programming Languages</em> (<strong>TAPL</strong>) (by Benjamin C. Pierce) [<a href="http://www.cis.upenn.edu/~bcpierce/tapl/">Homepage</a>]</li> |
| 143 | +<li><em>Advanced Topics in Types and Programming Languages</em> (<strong>ATTAPL</strong>) (by Benjamin C. Pierce) [<a href="http://www.cis.upenn.edu/~bcpierce/attapl/">Homepage</a>]</li> |
| 144 | +<li><em>Practical Foundations for Programming Languages</em> (<strong>PFPL</strong>) (by Robert Harper) [<a href="http://www.cs.cmu.edu/~rwh/plbook/book.pdf">PDF</a> (Online Preview)] [<a href="http://www.cs.cmu.edu/~rwh/plbook/2nded.pdf">PDF</a> (Working Draft)] [<a href="http://www.cs.cmu.edu/~rwh/courses/typesys/">Course Homepage</a> (CMU 15-814)] [<a href="http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%2207756bb0-b872-4a4a-95b1-b77ad206dab3%22">Course Videos</a> (CMU 15-819)]</li> |
| 145 | +<li><em>Type Theory and Functional Programming</em> (<strong>TTFP</strong>) (by Simon Thompson) [<a href="http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/">Homepage</a>] [<a href="http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf">PDF</a>]</li> |
| 146 | +<li><em>How to Prove It: A Structured Approach</em> (by Daniel J. Velleman)</li> |
| 147 | +<li><em>Proofs and Types</em> (<strong>ProT</strong>) (by Jean-Yves Girard, Yves Lafont, Paul Taylor) [<a href="http://www.paultaylor.eu/stable/Proofs+Types.html">Homepage</a>] [<a href="http://www.paultaylor.eu/stable/prot.pdf">PDF</a>]</li> |
| 148 | +<li><em>Implementing Mathematics with The Nuprl Proof Development System</em> (<strong>“NuPRL Book”</strong>) (by Robert L. Constable, etc.) [<a href="http://www.nuprl.org/book/">Homepage</a>] [<a href="http://www.cs.cornell.edu/info/projects/nuprl/book/doc.html">HTML</a>] [<a href="ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz">PS</a>]</li> |
| 149 | +<li><em>Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions</em> (<strong>Coq’Art</strong>) (by Yves Bertot, Pierre Castéran) [<a href="http://www.labri.fr/perso/casteran/CoqArt/index.html">Homepage</a>]</li> |
| 150 | +<li><em>Certified Programming with Dependent Types</em> (<strong>CPDT</strong>) (by Adam Chlipala) [<a href="http://adam.chlipala.net/cpdt/">Homepage</a>]</li> |
| 151 | +<li><em>Homotopy Type Theory</em> (<strong>HoTT</strong>) (by Univalent Foundations of Mathematics) [<a href="http://homotopytypetheory.org/book/">Homepage</a>] [<a href="https://github.com/HoTT/book">GitHub</a>]</li> |
| 152 | +</ul> |
| 153 | +</section> |
| 154 | +<section id="compiler-construction" class="level2"> |
| 155 | +<h2>Compiler Construction</h2> |
| 156 | +<p>[Wikipedia: <a href="https://en.wikipedia.org/wiki/Compiler_construction">Compiler construction</a>]</p> |
| 157 | +<p>Books:</p> |
| 158 | +<ul> |
| 159 | +<li><em>Language Implementation Patterns: Create Your Own Domain-Specific and General Programming Languages</em> (by Terence Parr)</li> |
| 160 | +<li><em>Lisp in Small Pieces</em> (<strong>L.i.S.P</strong>) (by Christian Queinnec) [<a href="http://pagesperso-systeme.lip6.fr/Christian.Queinnec/WWW/LiSP.html">Homepage</a>]</li> |
| 161 | +<li><em>The Implementation of Functional Programming Languages</em> (by Simon Peyton Jones) [<a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/">Homepage</a>] [<a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/slpj-book-1987.tar.gz">PDF</a>]</li> |
| 162 | +<li><em>Implementing Functional Languages: A Tutorial</em> (by Simon Peyton Jones, David Lester) [<a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/pj-lester-book/">Homepage</a>] [<a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/pj-lester-book/student.pdf.gz">PDF</a>]</li> |
| 163 | +<li><em>Programming Language Pragmatics</em> (by Michael L. Scott) [<a href="http://www.cs.rochester.edu/~scott/pragmatics/">Homepage</a>]</li> |
| 164 | +<li><em>Compilers: Principles, Techniques, and Tools</em> (<strong>“Dragon Book”</strong>) (by Alfred V. Aho, Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman) [<a href="http://dragonbook.stanford.edu/">Homepage</a>]</li> |
| 165 | +<li><em>Engineering a Compiler</em> (by Keith Cooper, Linda Torczon)</li> |
| 166 | +<li><em>Modern Compiler Implementation in ML</em> (<strong>MCIiML</strong>, <strong>“Tiger Book”</strong>) (by Andrew W. Appel) [<a href="http://www.cs.princeton.edu/~appel/modern/ml/">Homepage</a>]</li> |
| 167 | +<li><em>Compiling with Continuations</em> (<strong>CwC</strong>) (by Andrew W. Appel)</li> |
| 168 | +<li><em>Program Logics for Certified Compilers</em> (<strong>PLCC</strong>) (by Andrew W. Appel)</li> |
| 169 | +</ul> |
| 170 | +<hr /> |
| 171 | +<p><strong>Complementary Lists</strong></p> |
| 172 | +<ul> |
| 173 | +<li><a href="https://github.com/steshaw/plt-study" class="uri">https://github.com/steshaw/plt-study</a> - A path to programming language theory enlightenment (by Steven Shaw)</li> |
| 174 | +<li><a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml" class="uri">http://www.cis.upenn.edu/~bcpierce/courses/670Fall04/GreatWorksInPL.shtml</a> - Great works in programming languages (by Benjamin C. Pierce)</li> |
| 175 | +<li><a href="http://www.cs.cmu.edu/~crary/819-f09/" class="uri">http://www.cs.cmu.edu/~crary/819-f09/</a> - Classic papers in programming languages and logic (by Karl Crary)</li> |
| 176 | +<li><a href="http://alexott.net/en/fp/books/" class="uri">http://alexott.net/en/fp/books/</a> - Functional programming books overview (by Alex Ott)</li> |
| 177 | +<li><a href="http://www.cs.uu.nl/wiki/Techno/ProgrammingLanguageTheoryTextsOnline" class="uri">http://www.cs.uu.nl/wiki/Techno/ProgrammingLanguageTheoryTextsOnline</a> - Programming language theory texts online (by Frank Atanassow)</li> |
| 178 | +</ul> |
| 179 | +</section> |
| 180 | + </div> |
| 181 | + <footer> |
| 182 | + <!-- TO BE MODIFIED BY NEED --> |
| 183 | + <a title="Keyboard shortcut: q" |
| 184 | + href=".."> |
| 185 | + <i class="fa fa-angle-double-left" aria-hidden="true"></i> |
| 186 | + <code>Parent</code> |
| 187 | + </a> | |
| 188 | + <a class="raw" accesskey="r" |
| 189 | + title="Keyboard shortcut: R" |
| 190 | + href="https://wiki.soimort.org/plt/src.md"> |
| 191 | + <i class="fa fa-code" aria-hidden="true"></i> |
| 192 | + <code>Raw</code> |
| 193 | + </a> | |
| 194 | + <a class="history" accesskey="h" |
| 195 | + title="Keyboard shortcut: H" |
| 196 | + href="https://github.com/soimort/wiki/commits/gh-pages/plt/src.md"> |
| 197 | + <i class="fa fa-history" aria-hidden="true"></i> |
| 198 | + <code>History</code> |
| 199 | + </a> | |
| 200 | + <a class="edit" accesskey="e" |
| 201 | + title="Keyboard shortcut: E" |
| 202 | + href="https://github.com/soimort/wiki/edit/gh-pages/plt/src.md"> |
| 203 | + <i class="fa fa-code-fork" aria-hidden="true"></i> |
| 204 | + <code>Edit</code> |
| 205 | + </a> | |
| 206 | + <a title="Keyboard shortcut: p" |
| 207 | + href="javascript:window.print();"> |
| 208 | + <i class="fa fa-print" aria-hidden="true"></i> |
| 209 | + <code>Print</code> |
| 210 | + </a> | |
| 211 | + <a title="Keyboard shortcut: ." |
| 212 | + href="https://wiki.soimort.org/plt"> |
| 213 | + <i class="fa fa-anchor" aria-hidden="true"></i> |
| 214 | + <code>Permalink</code> |
| 215 | + </a> | |
| 216 | + Last updated: <span id="update-time"></span> |
| 217 | + </footer> |
| 218 | + </article></main> |
| 219 | + </body> |
| 220 | +</html> |
0 commit comments