Stephen A. Edwards Columbia University Fall 2008

http://www.cs.columbia.edu/~sedwards/classes/2010/w4115-spring/functional.pdf

http://www.amazon.com/Calculus-Semantics-Studies-Foundations-Mathematics/dp/0444875085 http://books.google.com/books/about/The_Lambda_Calculus.html?id=KbZFAAAAYAAJ http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.jsl/1183741496

Dana S. Scott University Professor Emeritus Carnegie Mellon University Visiting Scholar University of California, Berkeley

http://turing100.acm.org/lambda_calculus_timeline.pdf

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.6554

KAMAREDDINE, F. AND NEDERPELT, R. 1996b. A useful λ-notation. Theoretical Comput. Sci. 155, 1, 85–109. KLEENE, S

An historical survey on type theory can be found in Kamareddine et al.

AI Memo No. 349, December 1979

file:///Users/jasonwalsh/Dropbox/Books/AIM-349.pdf

http://repository.readscheme.org/ftp/papers/ai-lab-pubs/AIM-349.pdf

This brings up the point that the pedagogy of programming languages shouldn't start with the mathematical foundations: that battle has largely been lost in spite of the typing and proof approaches. It would be better to create something fun, play with the current best language available, then move to something more historical.

For example,

• CoffeeScript
• JavaScript
• Scheme
• Lambda Calculus
• Proof theory
• Logic

Would probably be best not to require that one conform directly to typing the language: though generally something that wouldn't be advised the building block approach might be reasonable.

Starts just by looking at the reasons by one would want to test their code: that's not a particularly good use of time since people buying the book presumeably understand the goals.

Looks initially just at the process for software development; likely a previous job from Mark Trostler?

• https://twitter.com/zzoass

Covered some interesting points:

https://www.math.ucla.edu/~asl/bsl/0704/0704-001.ps

… from Boole’s The Mathematical Analysis of Logic to Frege’s Begriffsschrift http://link.springer.com/chapter/10.1007/978-3-642-18026-2_10#page-2

http://orgmode.org/org.pdf

equivariance, freshness and abstraction.

http://mason.gmu.edu/~jgentle/csi9723/11s/l08b_11s.pdf

Definition. A group G is a nonempty set G together with a binary operation ◦ such that

• g1,g2 ∈ G ⇒ g1 ◦ g2 ∈ G (closure); • ∃e ∈ G ∀g ∈ G, e ◦ g = g (identity); • ∀g ∈ G ∃g −1 ∈ G 3 g −1 ◦ g = e (inverse); • g1,g2,g3∈ G ⇒ g 1 ◦ (g2 ◦ g3) = (g1 ◦ g2) ◦ g3 (associativity).

http://arxiv.org/pdf/cs/0607141v1.pdf

http://www.cl.cam.ac.uk/~amp12/papers/nomlfo/nomlfo-jv.pdf

http://www.inf.ed.ac.uk/teaching/courses/lp/

http://www.cl.cam.ac.uk/~amp12/talks/tacs01.pdf

The primary book for the programming side of the course is Learn Prolog Now, by Blackburn, Bos and Striegnitz. The book is strongly recommended, and is available free on-line. Other useful books on prolog programming are

Programming in Prolog by Clocksin and Mellish, Springer. (There are many copies of this in the University library.) The Art of Prolog by Sterling and Shapiro, MIT Press Prolog Programming for Artificial Intelligence by Ivan Bratko, Addison Wesley. For the theory lectures, the following background material on propositional and predicate will be useful for students who have not previously encountered propositional and predicate logic.

Wikipedia page on Propositional calculus Wikipedia page on First-order logic Wikipedia page on Structure (mathematical logic) Introductory slides (pdf) on Predicate logic and quantifiers from University of Nebraska

• https://dl.acm.org/citation.cfm?id=534538
• http://www.amazon.com/Introduction-Functional-Programming-Calculus-Mathematics/dp/0486478831

This was also listed under http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.9553 which looks interesting.

Alonzo Church Proceedings and Addresses of the American Philosophical Association Vol. 47, (1973 - 1974), pp. 21-33 Published by: American Philosophical Association Article Stable URL: http://www.jstor.org/stable/3129899

http://learnyouahaskell.com/

http://delivery.acm.org/10.1145/330000/321750/p160-rosen.pdf?ip=67.136.221.74&acc=ACTIVE%20SERVICE&CFID=197161644&CFTOKEN=63442998&__acm__=1364320374_27f40ba8627d0a8be785bcbf0431e82c

On Kindle.

• ch4: automatic promotion on overflow

http://pragprog.com/book/tbajs/async-javascript

You purchased this item on July 13, 2012.

http://www.comp.nus.edu.sg/~liangzk/papers/acns12.pdf

This had a number of the same points that we were planning on using for the fingerprinting.

Each of the parameters we were passing were going to be included in the list of privacy affected components.

http://web.cs.wpi.edu/~cew/papers/wosn10.pdf

Figure 3 shows three different mOSN interfaces where the mOSN identifier is leaked to a third-party server as part of a HTTP request via either the Request-URI or the Referer header.

JavaScript is a popular scripting language that is particularly useful for client-side programming together with HTML /XML on the Web. As JavaScript programs become more complex and large, separation of concerns at the implementation level is a significant challenge.

Similarly, return [expression,…]; was more common in ad-related scripts.

http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf

@incollection{Martin:2000:OP:331120.331143,
 author = {Martin, Robert C.},
 chapter = {The open-closed principle},
 title = {More C++ gems},
 editor = {Martin, Robert C.},
 year = {2000},
 isbn = {0-521-78618-5},
 pages = {97--112},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=331120.331143},
 acmid = {331143},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}

Listed in http://en.wikipedia.org/wiki/Open/closed_principle

The first principle in developing large software systems is the Open-Closed Principle (OCP). This principle seems asking for two conflict goals. How to realize the principle in the real software practice? What are the enabling technologies that can be used to implement the principle? This paper uses a case study to demonstrate the importance of the principle, the design methodology for realizing the principle, and its enabling technologies.

@inproceedings{Xu:2005:ROP:1090950.1091578,
 author = {Xu, Chong-wei and Hughes, Jose},
 title = {Realizing the Open-Closed Principle},
 booktitle = {Proceedings of the Fourth Annual ACIS International Conference on Computer and Information Science},
 series = {ICIS '05},
 year = {2005},
 isbn = {0-7695-2296-3},
 pages = {274--279},
 numpages = {6},
 url = {http://dx.doi.org/10.1109/ICIS.2005.107},
 doi = {10.1109/ICIS.2005.107},
 acmid = {1091578},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {Component-based Software Engineering, Software Reuse, Software Architecture, JavaBeans, Multithreading},
}

Looked at the delivery of JavaScript to make it non-blocking. The key notes are in

Picked up during the Fluent sale.

Program to an interface, not an implementation.

(quoted in )

• Get a short and digestible summary of ECMA-262, Edition 3, backed by real code you can run instantly
• Examine the creation of JavaScript objects
• Learn complex values, primitive values, scope, and inheritance
• Understand the importance of the head object
• Work with string, number, and Boolean objects and values
• Discover how to use the null value and the built-in math object
• Get into the details—beyond Mozilla’s reference guide for JavaScript 1.5

We present Dependent JavaScript (DJS), a statically typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible ob- jects, prototype inheritance, and arrays through a combina- tion of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies.

@article{Chugh:2012:DTJ:2398857.2384659,
 author = {Chugh, Ravi and Herman, David and Jhala, Ranjit},
 title = {Dependent types for JavaScript},
 journal = {SIGPLAN Not.},
 issue_date = {October 2012},
 volume = {47},
 number = {10},
 month = oct,
 year = {2012},
 issn = {0362-1340},
 pages = {587--606},
 numpages = {20},
 url = {http://doi.acm.org/10.1145/2398857.2384659},
 doi = {10.1145/2398857.2384659},
 acmid = {2384659},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {JavaScript, arrays, prototype inheritance, refinement types, strong updates},
}

JavaScript is the main scripting language for Web browsers, and it is essential to modern Web applications. Programmers have started using it for writing complex applications, but there is still little tool support available during development.

We present a static program analysis infrastructure that can infer detailed and sound type information for JavaScript programs using abstract interpretation. The analysis is designed to support the full language as defined in the ECMAScript standard, including its peculiar object model and all built-in functions. The analysis results can be used to detect common programming errors — or rather, prove their absence, and for producing type information for program comprehension.

@inproceedings{Jensen:2009:TAJ:1615441.1615460,
 author = {Jensen, Simon Holm and M{\o}ller, Anders and Thiemann, Peter},
 title = {Type Analysis for JavaScript},
 booktitle = {Proceedings of the 16th International Symposium on Static Analysis},
 series = {SAS '09},
 year = {2009},
 isbn = {978-3-642-03236-3},
 location = {Los Angeles, CA},
 pages = {238--255},
 numpages = {18},
 url = {http://dx.doi.org/10.1007/978-3-642-03237-0_17},
 doi = {10.1007/978-3-642-03237-0_17},
 acmid = {1615460},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@book{Souders:2009:EFW:1717800,
 author = {Souders, Steve},
 title = {Even Faster Web Sites: Performance Best Practices for Web Developers},
 year = {2009},
 isbn = {0596522304, 9780596522308},
 edition = {1st},
 publisher = {O'Reilly Media, Inc.},
}

This provides the core decision tree that is generally used when selecting loader. Applied heavily with some of the Canvas work but focussed more heavily when integrating with third-parties. See chapter 4 for the main distriction.

XHR Eval XHR Injection Script in Iframe Script DOM Elemnt Script Defer

• different domain
  • no order
  • preserve order
• same domain
  • no order
    • no busy
    • show busy
  • preserve order
    • no busy
    • show busy

In general for third-party JavaScript I've been looking at providing the no-order, async approach.

• Anarchy
• Utopia
• Physics
• Communication
• Sapir–Whorf Hypothesis http://c2.com/cgi/wiki?SapirWhorfHypothesis
• Whorfianism http://c2.com/cgi/wiki?WhorfianHypothesis

Contrast other books that note that the language used defines the ability to create abstractions.

@book{guin2009dispossessed,
  title={The Dispossessed},
  author={Guin, U.K.L.},
  isbn={9780061796883},
  url={http://books.google.com/books?id=k1Smynbdy\_IC},
  year={2009},
  publisher={HarperCollins}
}

• Transhumanism
• Cyborgs

Look at all of the fields available. Should there be an override?

Should there be encoding

Should this just be extra values.

http://tools.ietf.org/html/rfc6265#section-5.2

http://en.wikipedia.org/wiki/Babel-17

During an interstellar war one side develops a language, Babel-17, that can be used as a weapon. Learning it turns one into an unwilling traitor as it alters perception and thought. The change is made more dangerous by the language's seductive enhancement of other abilities.

• Neal Stephenson

http://en.wikipedia.org/wiki/Snow_Crash

http://en.wikipedia.org/wiki/JPod

• read while in Germany

http://en.wikipedia.org/wiki/Neuromancer

• Sprawl trilogy
• Gibson
• 1984
• Case (Henry Dorsett Case)

http://en.wikipedia.org/wiki/Count_Zero

• 1986
• Bobby Newmark

• 1988
• Mona
• Kumiko

http://en.wikipedia.org/wiki/Pattern_Recognition_(novel)

• Cayce Pollard
• Hubertus Bigend

Viral marketing with anonymous artistic clips.

• Hollis Henry
• Tito
• New York, Vancouver

http://en.wikipedia.org/wiki/Zero_History

• Hollis Henry
• Milgrim
• Gabriel Hounds
• Garreth
• London, Japan

We make monadic components more reusable and robust to changes by employing two new techniques for virtualizing the monad stack: the monad zipper and monad views. The monad zipper is a higherorder monad transformer that creates virtual monad stacks by ignoring particular layers in a concrete stack. Monad views provide a general framework for monad stack virtualization: they take the monad zipper one step further and integrate it with a wide range of other virtualizations. For instance, particular views allow restricted access to monads in the stack. Furthermore, monad views provide components with a call-by-reference-like mechanism for accessing particular layers of the monad stack.

In functional programming, monadic characterizations of computational effects are normally understood denotationally: they describe how an effectful program can be systematically expanded or translated into a larger, pure program, which can then be evaluated according to an effect-free semantics. Any effect-specific operations expressible in the monad are also given purely functional definitions, but these definitions are only directly executable in the context of an already translated program. This approach thus takes an inherently Church-style view of effects: the nominal meaning of every effectful term in the program depends crucially on its type.

In this paper we describe how to control aspect interference by construction by relying on the type system. More precisely, we combine a monadic embedding of the pointcut/advice model in Haskell with the notion of membranes for aspect-oriented programming. Aspects must explicitly declare the side effects and the context they can act upon. Allowed patterns of control flow interference are declared at the membrane level and statically enforced. Finally, computational interference between aspects is controlled by the membrane topology. To combine independent and reusable aspects and monadic components into a program specification we use monad views, a recent technique for conveniently handling the monadic stack.

In aspect-oriented programming (AOP), aspects are modular units that encapsulate crosscutting concerns. Aspects are typically developed independently, sometimes under the assumption that no other aspects will be applied to a system. However, when several aspects are applied on a system it is important to be aware of the interactions between them, because the correctness of the composed system may be affected.

This paper presents a monadic approach to incremental computation, suitable for purely functional languages such as Haskell. A program that uses incremental computation is able to perform an incremental amount of computation to accommodate for changes in input data. Recently, Acar, Blelloch and Harper presented a small Standard ML library that supports efficient, high-level incremental computations. Here, we present a monadic variant of that library, written in Haskell extended with first-class references. By using monads, not only are we able to provide a purely functional interface to the library, the types also enforce “correct usage” without having to resort to any type-system extension. We also find optimization opportunities based on standard monadic combinators.

Abstract Gifford and others proposed an effect typing discipline to de- limit the scope of computational effects within a program, while Moggi and others proposed monads for much the same purpose. Here we marry effects to monads, uniting two pre- viously separate lines of research. In particular, we show that the type, region, and effect system of Talpin and Jou- velot carries over directly to an analogous system for mon- ads, including a type and effect reconstruction algorithm. The same technique should allow one to transpose any ef- fect systems into a corresponding monad system.

http://www.grabmueller.de/martin/www/pub/Transformers.en.html

Monads are widely used in Haskell for modeling computational effects, but defining monads remains a daunting challenge. Since every part of a monad’s definition depends on its computational effects, programmers cannot leverage the common behavior of all monads easily and thus must build from scratch each monad that models a new computational effect.

This was from an article

Load scripts without blocking. As described in rule 6, external scripts block the download and rendering of other content in the page. This is true when the script is loaded in the typical way: <script src=”foo.js” type=”text/javascript”></script> Several techniques for downloading scripts, however, avoid this blocking behavior: • XHR eval • XHR injection • script in iframe • script DOM element • script defer • document.write script tag You can see these techniques illustrated in Cuzillion (http://stevesouders.com/cuzillion/), but as an example let’s look at the script DOM element approach: <script type=”text/javascript”> var se = document.createElement(‘script’); se.src = ‘http://anydomain.com/foo.js’; document.getElementsByTagName(‘head’). appendChild(se); </script>

@inproceedings{Rittri:1989:UTS:99370.99384,
 author = {Rittri, Mikael},
 title = {Using types as search keys in function libraries},
 booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
 series = {FPCA '89},
 year = {1989},
 isbn = {0-89791-328-0},
 location = {Imperial College, London, United Kingdom},
 pages = {174--183},
 numpages = {10},
 url = {http://doi.acm.org/10.1145/99370.99384},
 doi = {10.1145/99370.99384},
 acmid = {99384},
 publisher = {ACM},
 address = {New York, NY, USA},
}

A method is proposed to search for an identifier by using its type as a key. This can be seen as an approximation of using the specification as a key. Functions that only differ in their currying or argument order are essentially the same, which is expressed by a con- gruence relation on types. Isomorphism in Cartesian closed categories is used for this purpose. Simpler put, types are re- garded as congruent if they are equal under an arithmetical interpretation, with Cartesian product as multiplication and function space as exponentiation. The congruence is char- acterized by seven axioms, and there is an efficient decision algorithm. A search system for Lazy ML has been implemented; its performance is promising

@inproceedings{Runciman:1989:RRS:99370.99383,
 author = {Runciman, Colin and Toyn, Ian},
 title = {Retrieving re-usable software components by polymorphic type},
 booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
 series = {FPCA '89},
 year = {1989},
 isbn = {0-89791-328-0},
 location = {Imperial College, London, United Kingdom},
 pages = {166--173},
 numpages = {8},
 url = {http://doi.acm.org/10.1145/99370.99383},
 doi = {10.1145/99370.99383},
 acmid = {99383},
 publisher = {ACM},
 address = {New York, NY, USA},
}

ABSTRACT Polymorphic types are labels classifying both (a) degned components in a library and @) contexts of free variables in partially written programs. We propose to help programmers make better use of software libraries by providing a system that, given (b). identifies candidates from (a) with matching types. Assuming at first that matching means unifying (ie having a common instance) we discuss efficient ways of implementing such a retrieval system, and also indicate its likely effectiveness based on a quantitative study of currently available libraries. Later we introduce the applicative inamnce relation between types* which captures some iUttlitiOnS about generalisation/specialisation~ and discuss its use as the basis of a more flexible system.

On Lisp Prolog interpretter http://dunsmor.com/lisp/onlisp/onlisp_28.html

http://mitpress.mit.edu/sicp/full-text/book/book-Z-H-25.html#%_chap_4

Mentioned at #lambdajam

See also http://mitpress.mit.edu/sites/default/files/titles/content/sicm/book.html

http://norvig.com/paip.html

@InProceedings {Elliott2009-push-pull-frp,
  author    = {Conal Elliott},
  title     = {Push-pull functional reactive programming},
  booktitle = {Haskell Symposium},
  url       = {http://conal.net/papers/push-pull-frp},
  year      = 2009
}

http://conal.net/papers/push-pull-frp/

Functional reactive programming (FRP) has simple and powerful semantics, but has resisted efficient implementation. In particular, most past implementations have used demand-driven sampling, which accommodates FRP’s continuous time semantics and fits well with the nature of functional programming. Consequently, values are wastefully recomputed even when inputs don’t change, and reaction latency can be as high as the sampling period.

http://conal.net/papers/type-class-morphisms/

http://conal.net/papers/icfp97/

@InProceedings{ElliottHudak97:Fran,
  title        = {Functional Reactive Animation},
  url          = {http://conal.net/papers/icfp97/},
  author       = "Conal Elliott and Paul Hudak",
  booktitle    = "International Conference on Functional Programming",
  year         = 1997
}

Growing a Language Guy L. Steele Jr. Sun Microsystems Laboratories 1 Network Drive Burlington, Massachusetts 01803 guy.steele@sun.com October 1998