Kenn Knowles: Reading

August 2008

• Math/CS Books
  • Categories for the Working Mathematician. S MacLane.
  • Toposes, Triples, and Theories. M Barr, C Wells.
• Fiction
  • Kokoro. N Soseki.

July 2008

• Math/CS Books
  • Categories for the Working Mathematician. S MacLane.
  • Computational Homology. T Kaczynski, K Mischaikow, M Mrozek.
• Nonfiction
  • The Los Angeles River: Its Life, Death, and Possible Rebirth (Creating the North American Landscape). B Gumprecht.
  • City of Quartz: Excavating the Future in Los Angeles. M Davis.
  • The Omnivore's Dilemma. M Pollan.
• Fiction
  • Slow Learner. T Pynchon.
  • Learning the World. K MacLeod
  • Wilderness Tips. M Atwood.
  • Winter of Artifice. A Nin.
  • The Crying of Lot 49. T Pynchon.
  • Homebody. OS Card.
  • Kafka on the Shore. H Murakami.

June 2008

• Math/CS Books
  • Categories for the Working Mathematician. S MacLane.
  • Topology for Computing. AJ Zomorodian.
• Papers
  • Refunctionalization at work. O Danvy, K Millikin. MPC 2006.
  • A practical application of geometric semantics to static analysis of concurrent programs. E Goubault, E Haucourt. CONCUR 2005.
    
  • Model Checking Transactional Memories. R Guerraoui, TA Henzinger, B Jobstmann, V Singh. PLDI 2008.
• Nonfiction
  • Cradle to Cradle. W McDonough, M Braungart
  • Discipline and Punish. M Foucault.

May 2008

• Math/CS Books
  • Categories for the Working Mathematician. S MacLane.
  • Introduction to Smooth Manifolds. JM Lee.
  • Commonsense Reasoning. ET Mueller.
• Papers
  • State space reduction using partial order techniques. EM Clarke, O Grumberg, M Minea, D Peled. STTT 1999.
  • Lazy Satisfiability Modulo Theories. R Sebastiani. JSAT 2007.
  • Well-typed programs can't be blamed. P Wadler, RB Findler. Submitted to ICFP 2008.
  • Can We Make Mathematics Intelligible? RP Boas. American Mathematical Monthly 1981.
  • Losing Functions without Gaining Data - a new method for defunctionalisation. N Mitchell, C Runciman. Submitted to ICFP 2008.
  • A Monadic Approach for Avoiding Code Duplication When Staging Memoized Functions. K Swadi, W Taha, O Kiselov, E Pasalic. PEPM 2006.
  • That About Wraps it Up: Using FIX to Handle Errors Without Exceptions, and Other Programming Tricks. BJ McAdams. Tech Report 1997.
  • A Self-Hosting Evaluator using HOAS. E Barzilay. Scheme 2006.
  • Modularity and implementation of mathematical operational semantics. M Jaskelioff, N Ghani, G Hutton. Submitted to MSFP 2008.
  • Data Types a la Carte. W Swiestra.
  • Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. EM Clarke, EA Emerson, AP Sistla. TOPLAS 1986.
  • Model Checking and Abstraction. EM Clarke, O Grumberg, DE Long. TOPLAS 1992.
  • Counterexample-Guided Abstraction Refinement. EM Clarke, O Grumberg, S Jha, Y Lu, H Veith. CAV 2000.
• Presentations
  • Yices 1.0: An Efficient SMT solver (SMT-COMP'06 presentation). B Dutertre, L deMoura. STM-COMP 2006.
  • A Fast Linear Arithmetic Solver for DPLL(T). B Dutertre, L deMoura. CAV 2006.
  • BayFP 2008/05/08. B O'Sullivan. 2008.
• Fiction
  • For Whom the Bell Tolls. E Hemingway

April 2008

• Math/CS Books
  • Measure, Topology, and Fractal Geometry. GA Edgar.
• Papers
  • Generalized File System Dependencies. C Frost, M Mammarella, E Kohler, A Reyes, S Hovsepian, A Matsuoka, L Zhang. SOSP 2007.
  • Species: making analystic functors practical for functional programming. J Carette, G Uszkay. Submitted to MSFP 2008.
  • Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. P Cousot, R Cousot. POPL 1977.
  • An Analysis of Divisibility Orderings and Recursive Path Orderings. R Hasegawa. ASIAN 1997.
  • Deriving Structural Hylomorphisms From Recursive Definitions. Z Hu, H Iwasaki, M Takeichi. ICFP 1996.
  • Making Recursions Manipulable by Constructing Medio-Types. Z Hu, H Iwasaki, M Takeichi. Tech Report 1995.
  • A Parallel Solution to the Extended Set Union Problem with Unlimited Backtracking. MC Pinotti, VA Crupi, SK Das. IPPS 1996.
  • Beyond Myth and Metaphor - The Case of Narrative in Digital Media. ML Ryan. Game Studies 2001.
  • A Persistent Union-Find Data Structure. S Conchon, JC Filliatre. ML 2007.
  • Semi-Persistent Data Structures. S Conchon, JC Filliatre. ESOP 2008.
  • Fast Decision Procedures Based on Congruence Closure. G Nelson, DC Oppen. JACM 1980.
  • Design and synthesis of synchronization skeletons using branching time temporal logic. EM Clarke, EA Emerson. WLP 1981.
  • A Preliminary Poetics for Interactive Drama and Games. M Mateas. Digital Creativity 2001.
  • Model Checking Programs. W Visser, K Havelund, G Brat, SJ Park, F Lerda. ASE 2000.
  • Virtual Reality, Art, and Entertainment. J Bates. Presence 1992.
  • The Boehm-Jacopini Theorem is False, Propositionally. D Kozen, WL Tseng. MPC 2008.
  • Correct-by-Construction Concurrency. E Brady, K Hammond. Submitted to ICFP 2007.
  • Foundations for Structured Programming with GADTs. P Johann, N Ghani. POPL 2008.
  • The Essence of the Iterator Pattern. J Gibbons, B Oliviera. MSFP 2006.
• Presentations
  • Principles of Graph Drawing. D Eppstein. 2008.
• Nonfiction
  • Game Design as Narrative Architecture. Henry Jenkins. In First Person: New Media as Story, Performance and Game.
  • Toward Computer Game Studies. Markku Eskelinen. In First Person: New Media as Story, Performance and Game.
  • Genre Trouble. Espen AarsethoIn First Person: New Media as Story, Performance and Game.
  • Interactivity. Chris Crawford on Game Design. C Crawford. Chapter 6.
  • Lord Burleigh's Kiss. Hamlet on the Holodeck. J Murray. Chapter 1.
  • Avatars of Story. ML Ryan.
  • The Structure Spectrum. Story: Substance, Structure, Style, and The Principles of Screenwriting. J McKee. Chapter 1.
  • The Substance of Story. Story: Substance, Structure, Style, and The Principles of Screenwriting. J McKee. Chapter 7.
• Fiction
  • The Wind's Twelve Quarters. UK LeGuin.

March 2008

• Math/CS Books
  • A Mathematical Gift, I. K Ueno, K Shiga, S Morita.
  • The Knot Book. C Adams.
  • Algebra with Galois Theory. E Artin.
• Papers
  • A Type-Theoretic Approach to Higher-Order Modules with Sharing.. R Harper, M Lillibridge. POPL 1994.
• Nonfiction
  • 1794: America, Its Army, and the Birth of a Nation. D R Palmer.
  • The Problems of Philosophy. B Russell.
  • Chaos: Making a New Science. J Gleick.
  • Turbulent Mirror: An Illustrated Guide to Chaos Theory and the Science of Wholeness. J Briggs, FD Peat.

February 2008

• Math/CS Books
  • The Probabilistic Method. N Alon, J H Spencer.
  • Probability Models for Computer Science. S M Ross.
• Papers
  • Monads for Incremental Computing. M Carlsson. ICFP 2002.
  • Monadic Memoization Mixins. D Brown, WR Cook. Tech Report 2007.
• Nonfiction
  • The God Delusion. R Dawkins.
  • Animal, Vegetable, Miracle. B Kingsolver.

January 2008

• Math/CS Books
  • Pearls in Graph Theory. N Hartsfield, G Ringel.
  • Isomorphisms of Types. R DiCosmo.
  • Randomized Algorithms. R Motwani, P Raghavan.
• Papers
  • Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. J Maraist, M Odersky, D Turner, P Wadler. MFPS 1995.
  • Selective Memoization. U Acar, GE Blelloch, R Harper. POPL 2003.
  • A Short Cut to Deforestation. A Gill, J Lauchbury, SLP Jones. FPCA 1993.
  • The Concatenate Vanishes. P Wadler. 1989.
  • A novel representation of lists and its application to the function "reverse". RJM Hughes. Information Processing Letters. 1986
  • Continuation-Based Program Transformation Strategies. M Wand. JACM 1980.
  • Defunctionalization at Work. O Danvy, LR Nielsen. PPDP 2001.
  • A Call-By-Need Lambda Calculus. Z Ariola, M Felleisen, J Maraist, M Odersky, P Wadler. POPL 1995.
• Fiction
  • Enchantment. OS Card.
  • Oryx and Crake. M Atwood.

December 2007

• Math/CS Books
  • Euler: The Master of us All. W Dunham
  • Four Colors Suffice. R Wilson.
  • The Four Pillars of Geometry. J Stillwell.
• Papers
  • An Introduction to Knuth-Bendix Completion. AJJ Dick. CJ 1991.
  • A Beginner's Guide to Forcing T Chow. 2007.
  • SAC: Off-the-shelf Support for Data-parallelism on Multicores. C Greick, SB Scholz. DAMP 2007.
  • On Equivalence and Canonical Forms in the LF Type Theory. R Harper, F Pfenning. TOCL 2005.
  • Unfolding Pointer Algorithms. R Bird. JFP 2001.
  • Probabilistic Functional Programming in Haskell. M Erwig, S Kollmansberger. JFP 2006.
  • Applicative programming with effects. C McBride, R Paterson. JFP 2007.
  • The Essence of Dataflow Programming. T Uustalu, V Vene. CEFP 2005.
  • Genuinely Functional User Interfaces. A Courtney, C Elliott. Haskell 2001.
  • The Yampa Arcade. A Courtney, H Nilsson, J Peterson. Haskell 2003.
• Fiction
  • Snow Crash. N Stephenson.
  • Blackgod. J Gregory Keyes.
• Nonfiction
  • The End of Physics. David Lindley.

November 2007

• Math/CS Books
  • Symmetries. DL Johnson.
  • A Geometrical Picture Book. B Polster.
• Papers
  • Dependent Types for Distributed Arrays. W Swierstra, T Altenkirch. Submitted 2007.
  • Random Access to Abstract Data Types. M Erwig. AMAST 2000.
  • Metamorphic Programming: Structured Recursion for Abstract Data Types. M Erwig. Tech Report.
  • The Categorical Imperative - Or: How to Hide your State Monads. M Erwig. IFL 1998.
  • Lightweight concurrency primitives for GHC. P Li, A Tolmach, S Marlow, SP Jones. Haskell 2007.
  • Type-indexed data types. R Hinze, J Jeuring, A Loh. SCP 2004.
  • Composing monads using coproducts. C Lüth, N Ghani. ICFP 2002.
  • The high-level parallel language ZPL improves productivity and performance. BL Chamberlain, SE Choi, SJ Deitz, L Snyder. P-PHEC 2004.
  • Abstractions for dynamic data distribution. SJ Deitz, BL Chamberlain, L Snyder HIP 2004.
  • High-level language support for user-defined reductions. SJ Deitz, BL Chamberlain, L Snyder. Supercomputing 2002.
  • Recycling continuations. J Sobel, DP Friedman. ICFP 1998.
  • Clowns to the Left of me, Jokers to the Right: Dissecting Data Structures. C McBride. POPL 2008.
  • Dealing with Large Bananas. R Lammel, J Visser, J Kort. WGP 2000.
  • Sequential algorithms, deterministic parallelism, and intensional expressiveness. S Brookes. D Dancanet. POPL 1995.
  • Fold and Unfold for Program Semantics. G Hutton. ICFP 1998.
• Presentations
  • A Comic Book Introduction to ZPL.
• Fiction
  • The Tower on the Rift. I Irvine.
  • Dark is the Moon. I Irvine.
  • The Way Between the Worlds. I Irvine.

October 2007

• Math/CS Books
  • Foundations of Parallel Programming. D Skillicorn
  • Characteristic Classes. J Milnor, J D Stasheff.
  • Algebraic Topology. A Hatcher.
  • Special Relativity. NMJ Woodhouse.
• Papers
  • Commutativity Analysis: A New Analysis Framework for Parallelizing Compilers. MC Rinard, PC Diniz. PLDI 1996.
  • Feedback directed implicit parallelism T Harris, S Singh. ICFP 2007.
  • Rolling your own mutable ADT—a connection between linear types and monads. CP Chen, P Hudak. POPL 1997.
  • More Types for Nested Data Parallel Programming. MMT Chakravarty, G Keller. ICFP 2000.
  • Higher Order Flattening. R Leshchinskiy, MMT Chakravarty, G Keller. PAPP 2006
  • Promotional Transformation on Monadic Programs. Z Hu, H Iwasaki, M Takeichi. Tech Report 1995.
  • An initial-algebra approach to directed acyclic graphs. J Gibbons. MPC 1995.
  • Sorting Morphisms. L Augusteijn. AFP 1998.
  • Parallel and Distributed Haskells. PW Trinder, HW Loidl, RF Pointon. JFP 2002.
  • Bringing Skeletons out of the Closet: A Pragmatic Manifesto for Skeletal Parallel Programming. M Coll. Parallel Computing 2004.
  • An Accumulative Parallel Skeleton for All. Z Hu, H Iwasaki, M Takeichi. ESOP 2002.
  • Programming Parallel Algorithms. G Blelloch. CACM 1996.
  • Higher Order Flattening. R Leshchinskiy, MMT Chakravarty, G Keller. PAPP 2006.
  • Oriented Matroids: The Power of Unification. J Malkevitch. AMS 2003.
  • Matroids: The Value of Abstraction. J Malkevitch. AMS 2003.
  • Data-Distributions in PowerList Theory. V Niculescu. ICTAC 2007.
  • Lifting Abstract Interpreters to Quantified Logical Domains. S Gulwani, B McCloskey, A Tiwari. Tech Report 2007.
  • A tutorial on the universality and expressiveness of fold. G Hutton. JFP 1999.
  • Generic programming with functors and relations. RS Bird, O DeMoor, P Hoogendijk. JFP 1996.
  • A Pure Language with Default Strict Evaluation Order and Explicit Laziness. T Sheard. Haskell 2003.
  • Equational Code Generation: Implementing Categorical Data Types for Data Parallelism. DB Skillicorn, W Cai. TENCON 1994.
  • Structuring data parallelism using categorical data types DB Skillicorn. PMMP 1993.
  • Subtyping and Inheritance for Categorical Datatypes. E Poll. TTP 1998.
  • Parallel Functional Programming: An Introduction. K Hammond. 1994.
  • Rolling your own mutable ADT—a connection between linear types and monads. CP Chen, P Hudak. POPL 97.
  • Skeletons, List Homomorphisms and Parallel Program Transformation. Z Grant-Duff, P Harrison. Tech Rpt 1994.
  • Categorical Data Types. DB Skillicorn. 1993.
  • A gentle introduction to semantic subtyping G Castagna, A Frisch. PPDP 2005.
  • Some Topologies for Computation. G Longo. 2001.
• Presentations
  • pH: Lessons Learned. JW Maessen. DPMC 2006.
  • Nesl. G Blelloch. DPMC 2006.
  • Now You C It. Now You Don’t!. R Ennals. DPMC 2006.
  • Hume and Multicore Architectures. K Hammond. DPMC 2006.
  • Design and Implementation Issues for Atomicity and Functional Languages. D Grossman. DPMC 2006.
  • Nested Data Parallelism in Haskell. M. Chakravarty. DPMC 2006.
  • Stabilizers: A Safe Lightweight Checkpointing Abstraction for Concurrent Programs. S Jaganathan. DPMC 2006.
• Fiction
  • The Waterborn. JG Keyes.
  • Dune. F Herbert.
  • A Shadow on the Glass. I Irvine.

September 2007

• Math/CS Books
  • Logic for Mathematics and Computer Science. S Burris.
  • Fundamentals of Complex Analysis. E Saff, A Snider.
  • Complex Variables and Applications. J Brown, R Churchill.
  • Essential Topology. M Crossley.
• Papers
  • Program Specification and Data Refinement in Type Theory. Z Luo. MCSC 1993.
  • Extensible Pattern Matching via a Lightweight Language Extension. D Syme, G Neverov, J Margetson. ICFP 2007.
  • A Coinductive Monad for Prop-Bounded Recursion. A Megacz. PLPV 2007.
  • Extended static checking of call-by-value functional programs. F Pottier, Y Régis-Gianas. Submitted July 2007.
• Nonfiction
  • In the Realm of a Dying Emperor. N Field.
• Fiction
  • Seventh Son. O S Card.

August 2007

• Math/CS Books
  • Topoi: The Categorical Analysis of Logic. R Goldblatt.
  • Fearless Symmetry. A Ash, R Gross.
  • Yearning for the Impossible. J Stillwell.
  • The Pea and the Sun. L Wapner.
  • Journey Though Genius. W Dunham.
  • Unknown Quantity. J Derbyshire.
• Papers
  • Embedding Prolog in Haskell. M Spivey, S Seres. Haskell 1999.
  • Down with the bureaucracy of syntax! Pattern matching for classical linear logic. P Wadler. 2004.
  • Explaining Binomial Heaps. R Hinze. JFP 1999.
  • Relationally-Parametric Polymorphic Contracts. A Guha, J Matthews, R Findler, S Krishnamurthi. DLS 2007.
  • A Categorical Manifesto. J Goguen. MSC 1991.
  • Proof-Directed Debugging. R Harper. JFP 1999.
  • A Type Discipline for Authorization in Distributed Systems. C Fournet, A Gordon, S Maffeis. CSF'07
  • Codata and Comonads in Haskell. R Kieburtz. 1999
  • A modern eye on ML type inference: old techniques and recent developments. F Pottier. APPSEM 2005.
  • How to prove higher-order theorems in first-order logic. M Kerber. IJCAI 1991.
  • A Type Discipline for Authorization Policies. C Fournet, A Gordon, S Maffeis. ESOP 2005.
  • Bananas in Space: Extending Fold and Unfold to Exponential Types. E Meijer, G Hutton. FPCA 1995.
  • Type Classes with Existential Types. K Läufer. JFP 1996.
• Presentations
  • Beyond Classical Domain Theory. A Simpson. MFPS 2007.
• Fiction
  • Malafrena. U LeGuin.

July 2007

• Math/CS Books
  • ''The Birth of Model Theory: Lowenheim's Theorem in the Frame of the Theory of Relatives.'' C Badesa.
  • Counterexamples in Topology. LA Steen, JA Seebach.
  • Conceptual Mathematics: A First Introduction to Categories. F W Lawvere, S H Schanuel.
  • Topology. J Munkres.
  • Topoi: The Categorical Analysis of Logic. R Goldblatt.
  • Imagining Numbers. B Mazur.
• Fiction
  • Mortal Engines. S Lem.
  • After the Quake. H Murakami.
  • Hocus Pocus. K Vonnegut.
  • Strange Candy. L Hamilton.
  • The Word for World is Forest. U LeGuin.

June 2007

• Math/CS Books
  • ''The Birth of Model Theory: Lowenheim's Theorem in the Frame of the Theory of Relatives.'' C Badesa.
  • Counterexamples in Topology. LA Steen, JA Seebach.
  • Proofs and Types. JY Girard.
  • Basic Topology. MA Armstrong.
  • Categories for Everybody. S Awodey.
  • Conceptual Mathematics: A First Introduction to Categories. F W Lawvere, S H Schanuel.
  • Topology. J Munkres.
• Papers
  • A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Adam Chlipala. PLDI 2007.
  • Optimistic Parallelism Requires Abstractions. M Kulkarni, K Pingali, B Walter, G Ramanarayanan, K Bala, LP Chew. PLDI 2007.
  • Nondeterminism and Language Design in Deep Inference. O Kahramanogullari. PhD 2006.
  • Linear Logic and Noncommutativity in the Calculus of Structures. L Straßburger. PhD 2003.
  • Deep Inference and Symmetry in Classical Proofs. K Brünnler. PhD 2004.
  • Automatic Inversion Generates Divide-and-Conquer Parallel Programs. K Morita, A Morihata, K Matsuzaki, Z Hu, M Takeichi. PLDI 2007

May 2007

• Math/CS Books
  • Transactional Memory. J Larus and R Rajwar.
  • Topoi, The Categorical Analysis of Logic. R Goldblatt.
  • Categorical Logic and Type Theory. B Jacobs.
  • Algebra of Programming. R Bird, O DeMoor.
  • Algebra. S Maclane, G Birkhoff.
• Papers
  • Data Parallel Haskell: a status report. M Chakravarty, R Leshchinskiy, SP Jones, G Keller, S Marlow. 2007.
  • Algorithm + Strategy = Parallelism. PW Trinder, K Hammond, HW Loidl, SLP Jones. JFP 1998.
  • Deep Inference and Its Normal Form of Derivations. K Brünnler. CiE 2006.
  • Mismatch. A Guglielmi. 2003.
  • Automatic Mutual Exclusion. M Isard, A Birrell. HotOS 2007.
  • Deconstructing Transactional Semantics: The Subtleties of Atomicity. C Blundell, EC Lewis, M Martin. WDDD 2005.
  • Compiler and Runtime Support for Efficient Software Transactional Memory. AR Adl-Tabatabai, B Lewis, V Menon, B Murphy, B Saha, T Shpeisman. PLDI 2006.
  • McRT-STM: A High Performance Software Transactional Memory System for a Multi-Core Runtime. B Saha, AR Adl-Tabatabai, R Hudson, C Minh, B Hertzberg. PPoPP 2006.
  • Tasking with Out-of-Order Spawn in TLS Chip Multiprocessors: Microarchitecture and Compilation. J Renau, J Tuck, W Liu, L Ceze, K Strauss, J Torrellas. ICS 2005.
  • Energy-Efficient Thread-Level Speculation on a CMP. J Renau, K Strauss, L Ceze, W Liu, S Sarangi, J Tuck, J Torrellas. TOPPICKS 2005.
  • Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs. A Abel, T Coquand. TLCA 2005.
  • Fine-grained Visualization Pipelines and Lazy Functional Languages. D Duke, M Wallace, R Borgo, C Runciman. VCG 2006.
  • Beautiful Concurrency. SP Jones. 2007
  • Composable Memory Transactions. T Harris, S Marlow, SP Jones, M Herlihy. PPoPP 2005.
  • Practical Type Inference Based on Success Typings. T Lindahl, K Sagonas. PPDP'06
  • A Practical Subtyping System for Erlang. S Marlow and P Wadler. ICFP'97
  • Process structuring, synchronization, and recovery using atomic actions. D Lomet. LDRS 1977.
  • Language Support for Lightweight Transactions. T Harris, K Fraser.
  • Exceptions and side-effects in atomic blocks. T Harris.
  • Logical equivalence for subtyping and recursive types. S van Bakel, U deLiguoro. TCS 2006.
  • Stream Fusion: From Lists to Streams to Nothing at All. D Coutts, R Leshchinskiy,D Stewart. Submitted 2007.
• Presentations
  • A Bisimulation for Type Abstraction and Recursion. E Sumii, B Pierce. POPL 2005.
  • CS 294-9 Fall 2006 @ Berkeley
• Fiction
  • My Uncle Oswald. R Dahl.
  • ''Howl's Moving Castle.'' DW Jones.

April 2007

• Math/CS Books
  • A Practical Introduction to denotational semantics. Lloyd Allison.
  • Abstract Algebra. D Dummit, R Foote
  • Algebra of Programming. R Bird, O DeMoor.
  • Algebra. S Maclane, G Birkhoff.
• Papers
  • The Landscape of Parallel Computing Research: A View from Berkeley. K Asanovic, R Bodik, BC Catanzaro, JJ Gebis, P Husbands, K Keutzer, D Patterson, WL Plishker, J Shalf, SW Williams, K Yelick.
  • Linearizability: a correctness condition for concurrent objects. M Herlihy, J Wing. TOPLAS 1990.
  • System F with Type Equality Coercions. M Sulzmann, M Chakravarty, SP Jones. 2006.
  • Multilisp: A Language for Concurrent Symbolic Computation. R Halstead. TOPLAS 1985.
  • A Minicourse on Multithreaded Programming. C Leiserson, H Prokop. 1998.
  • Interpreting the Data: Parallel Analysis with Sawzall. R Pike, S Dorward, R Griesemer, S Quinlan. SPJ 2005.
  • Theorems for free! P Wadler. FPCA 1989.
  • Dependent types in practical programming. H Xi, F Pfenning. POPL 1999.
  • Church's Thesis and Functional Programming. D Turner. "Church's Thesis after 70 Years" 2006.
  • Transactional memory with data invariants. T Harris, SP Jones. TRANSACT 2006.
  • Haskell on a shared-memory multiprocessor. T Harris, S Marlow, SP Jones. Haskell 2005.
  • Google's MapReduce Programming Model -- Revisited. R Lämmel. Draft 2007.
  • Hoare Logic for Realistically Modelled Machine Code. M Myreen, M Gordon. TACAS 2007.
  • On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning. X Feng, R Ferreira, Z Shao. ESOP 2007.
  • Abstract Predicates and Mutable ADTs in Hoare Type Theory. A Nanevski, G Morrisett, L Birkedal. ESOP 2007.
  • Subtyping Parametric and Dependent Types -- An Introduction. G Chen, G Longo
  • A Principled Approach to Version Control. A Löh, W Swierstra, D Leijen. Draft 2007.
  • Developing a high-performance web server in Concurrent Haskell. S Marlow. JFP 2003.
  • Concurrent Haskell. SP Jones, A Gordon, S Finne. POPL 1996.
  • Static Error Detection Using Semantic Inconsistency Inference. I Dillig, T Dillig, A Aiken. PLDI 2007.
  • First-Class Synchronous Operations. J Reppy. TPPP 1995.
  • Concurrent ML: Design, Application, and Semantics. J Reppy. PCSA 1992.
  • Introduction to Generalized Type Systems. H Barendregt. 1991.
  • Data Types are Values. J Donahue, A Demers. TOPLAS 1985.
  • Combined Satisfiability Modulo Parametric Theories. S Krstic, A Goel, J Grundy, C Tinelli.
  • An Introduction to Programming with Threads. A Birrell.
  • An Introduction to Programming with C# Threads. A Birrell, D Ilstrup.
  • Threads Cannot Be Implemented As a Library. H Boehm. PLDI 2005.
  • The Java Memory Model. J Manson, W Pugh, S Adve. POPL 2005.
  • The Java Memory Model is Fatally Flawed. W Pugh.
  • Logic and Programming Languages. D Scott. CACM 1977.
• Presentations
  • Coinduction in programming languages. D Sangiorgi. POPL 2004.
  • Bisimulation and coinduction: from the origins to today. D Sangiorgi. LICS 2004.
• Fiction
  • The Once and Future King. T.H. White.
  • Stranger in a Strange Land. R Heinlein.

March 2007

• Math/CS Books
  • The Development of Categorical Logic. J Bell. Preprint 2007.
  • Programming Languages: Application and Interpretation. S Krishnamurthi. Version 2006-01-15.
• Papers
  • A short survey of isomorphisms of types. R Di Cosmo. MSC 2005.
  • Fully Persistent Data Structures for Disjoint Set Union Problems. G Italiano, N Sarnak. WADS 1991.
  • State in Haskell. J Launchbury, SP Jones. LISP 1995.
  • Expressing Heap-shape Contracts in Linear Logic. F Perry, L Jia, D Walker. GPCE 2006.
  • A Pointless Derivation of Radixsort. J Gibbons. JFP 1998.
  • Derivatives of Regular Expressions. J Brzozowski. JACM 1964.
  • Lazy Assertions. O Chitil, D McNeill, C Runciman. IFL 2003.
  • A Logical View of Effects. S Park, R Harper. 2004
  • Type inference with non-structural subtyping. J Palsberg, M Wand, P O'Keefe. FAoC 1997.
  • Efficient inference of partial types. D Kozen, J Palsberg, MI Schwartzbach. FoCS 1992.
  • Syntactic Logical Relations for Polymorphic and Recursive Types. K Crary, B Harper. Gordon Plotkin Festschrift.
  • Sound and complete models of contracts. M Blume, D McAllester. JFP 2006.
  • Subtyping and Inheritance for Categorical Datatypes. E Poll. TTP-Kyoto 1997.
  • A Functional Description of TeX's Formula Layout. R Heckmann, R Wilhelm. JFP 2000.
  • Equational axiomatization of bicoercibility for polymorphic types. J Tiuryn. FSTTCS 1995.
• Presentations
  • Dependent Types. R Harper. 2002.
  • A Lexer for Haskell in Haskell. T Hallgren. 2002.
  • Command-Line Parsing Combinators. T Hallgren. 2005.
  • Towards Dependent Types over Programmer-Defined Index Domains. D Licata, R Harper. 2005.
• Videos (not really reading, but I'm really enjoying these, and they are academically related)
  • DanFest 2004
  • GHC Hackathon 2006
• Nonfiction
  • The Haiku Handbook. W Higginson, P Harter.
  • The Haiku Form. J Giroux.
  • Haiku in English. H Henderson.
  • Okinawan Diaspora.R Nakasone (Editor)
  • The Mythical Man-Month. FP Brooks.
• Fiction
  • Elemental. S Saville, A Kontis (Editors)

February 2007

• Math/CS Books
  • Categories for Types. R Crole.
  • Isabelle/HOL: A Proof Assistant for Higher-Order Logic. T Nipkow, L Paulson, M Wenzel.
  • Topology and Category Theory in Computer Science. G M Reed, A W Roscoe, R F Wachter, editors.
  • Algebra. S Maclane, G Birkhoff.
• Papers
  • A tutorial on (co) algebras and (co) induction. B Jacobs, J Rutten. 1997.
  • Types, Bytes, and Separation Logic. G Klein, H Tuch, M Norrish. POPL 2007.
  • Context Logic as Modal Logic: Completeness and Parametric Inexpressivity. C Calcagno, P Gardner, U Zarfaty. POPL 2007.
  • Cork: Dynamic Memory Leak Detection for Garbage-Collected Languages. M Jump, K S McKinley. POPL 2007.
  • Dynamic Heap Type Inference for Program Understanding and Debugging. M Polishchuk, B Liblit, C W Schulze. POPL 2007.
  • Compositional Dynamic Test Generation. P Godefroid. POPL 2007.
  • Dynamic Typing: Syntax and Proof Theory. F Heinglein. SCP 1994.
  • Typed Contracts for Functional Programming. R Hinze, J Jeuring, A Löh. FLOPS 2006.
  • Defining functions on equivalence classes. L Paulson. TOCL 2006.
  • Predicate Subtyping with Predicate Sets. J Hurd. TPHOLs 2001.
  • State of the Union: Type Inference via Craig Interpolation. R Jhala, R Majumdar, R Xu. TACAS 2007.
  • Gradual Typing for Objects. J Siek, W Taha. ECOOP 2007.
  • A Head-to-Head Comparison of de Bruijn Indices and Names. S Berghofer, C Urban. LFMTP 2006.
  • Total Functional Programming. D Turner. JUCS 2004.
  • Nominal Unification. C Urban, A Pitts, M Gabbay. CSL 2003.
  • Generic Properties of Datatypes. R Backhouse, P Hoogendijk. GP 2004.
  • When Do Data Types Commute? P Hoogendijk, R Backhouse. CCTC 1997.
  • Domains and Denotational Semantics: History, Accomplishments and Open Problems. A Jung, editor. M Fiore, E Moggi, P O'Hearn, J. Riecke, G Rosolini, I Stark. Bulletin of the European Association for Theoretical Computer Science. 1996.
  • Formal Proof Sketches. F Wiedijk. TPP 2004.
  • Structured calculational proof. R Back, J Grundy, J von Wright. FAC 1997.
  • A Rewriting Semantics for Type Inference. G Kuan, D Macqueen, R Findler. ESOP 2007.
  • Principal Type Schemes for Modular Programs. D Dreyer, M Blume. ESOP 2007.
  • How to write a proof. L Lamport. American Mathematical Monthly. 1995.
  • Why Dependent Types Matter. T Altenkirch, C McBride, J McKinna. Manuscript 2005.
  • A Very Modal Model of a Modern, Major, General Type System. A Appel, P Mellies, C Richards, J Vouillon. POPL 2007.
  • A locally nameless solution to the POPLmark challenge. X Leroy. Tech report 2007.
  • Nominal Reasoning Techniques in Coq (Extended Abstract). B Aydemir, A Bohannon, S Weirich. LFMTP 2006.
  • Developing (Meta)Theory of lambda-calculus in the Theory of Contexts. M Miculan. MERLIN 2001.
  • Translating specifications from nominal logic to CIC with the theory of contexts. M Miculan, I Scagnetto, F Honsell. MERLIN 2005.
  • Categorical Logic. A Pitts. Tech report 1995.
• Presentations
  • CSCI 7000-000 (1). Current Topics in Computer Science: Practical Theorem Proving with Isabelle/Isar. Taught by J Siek. 2007.
  • The Role of the Study of Programming Languages in the Education of a Programmer. D Friedman.
  • Reasoning About Languages with Binding. R Pollack. 2006.

January 2007

• Math/CS Books
  • Topology Via Logic. S Vickers.
  • Topology. J Munkres.
  • Abstract Algebra. D Dummit, R Foote
  • Algebra of Programming. R Bird, O DeMoor.
  • Basic Category Theory for Computer Scientists. B Pierce.
• Papers
  • Dependent Types for Low-Level Programming. J Condit, M Harren, Z Anderson, D Gay, G Necula. ESOP 2007.
  • QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. K Claessen, J Hughes. ICFP 2000
  • DART: Directed Automated Random Testing. P Godefroid, N Klarlund, K Sen. PLDI 2005
  • EXE: Automatically Generating Inputs of Death. C Cadar, V Ganesh, P Pawlowski, D Dill, D Engler. To appear: CCCS 2006.
  • Safe Manual Memory Management in Cyclone. N Swamy, M Hicks, G Morrisett, D Grossman, T Jim. SCP 2006.
  • Memory Management with Use-Counted Regions. T Terauchi, A Aiken. Technical Report UCB/CSD-4-1314 2004.
  • Ownership types for safe region-based memory management in real-time Java. C Boyapati, A Salcianu, W Beebee Jr, M Rinard. PLDI 2003.
  • A Type System for Statically Detecting Spreadsheet Errors. Y Ahmad, T Antoniu, S Goldwater, S Krishnamurthi. ASE 2003.
  • Type Inference for Spreadsheets. R Abraham, M Erwig. PPDP 2006.
  • Exception handling in the spreadsheet paradigm. M Burnett, A Agrawal, P van Zee. SE 2000.
  • High-level views on low-level representations. I Diatchki, MP Jones, R Leslie. ICFP 2005.
  • A principled approach to operating system construction in Haskell. T Hallgren, MP Jones, R Leslie, A Tolmach. ICFP 2005.
  • Running the Manual: An Approach to High-Assurance Microkernel Development. P Derrin, K Elphinstone, G Klein, D Cock, M Chakravarty. Haskell 2006.
  • Strongly Typed Memory Areas: Programming Systems-Level Data Structure in a Functional Language. I Diatchki, MP Jones. Haskell 2006.
• Nonfiction
  • Okinawa: History of an Island People. G Kerr.
  • Account of a Voyage of Discovery. B Hall.
• Fiction
  • World of Exile. U LeGuin.
  • The Curse of Chalion. L M Bujold.
  • Foreigner. C. J. Cherryh.
  • Goodbye Tsugumi. B Yoshimoto.

Winter 2006 (stuff from just before this quasiblog existed that sticks in my memory)

• Math/CS Books
  • Conceptual Mathematics: A First Introduction to Categories. F W Lawvere, S H Schanuel.
  • Interactive Theorem Proving and Program Development. Y Bertot, P Castéran.
• Papers
  • Synthetic topology of data types and classical spaces. M Escardo. ENTCS 1987.
• Nonfiction
  • The Northern World. D Wilson.
  • The Battle for Okinawa. H Yahara, F Gibney.
• Fiction
  • The Lathe of Heaven. U LeGuin.
  • The Left Hand of Darkness. U LeGuin.
  • Unlocking The Air and other stories. U LeGuin
  • Southern Exposure. M Molasky, S Rabson, editors.
  • Hard-Boiled Wonderland and the End of the World. H Murakami.
  • Hardboiled and Hard Luck. B Yoshimoto.
  • Kitchen. B Yoshimoto.
  • Norwegian Wood. H Murakami.
  • Palm of the Hand Stories. Y Kawabata.
  • The House of Sleeping Beauties and other stories. Y Kawabata.
  • 「掌の小説」川端 康成
  • 「あずまんが大王」東清彦