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