Presention by Adam Chlipala on Ur/Web - Plus Time for Networking

This Meetup will feature a presentation on Ur/Web (http://www.impredicative.com/ur/) - a domain-specific functional language for web applications - by Adam Chlipala from MIT CSAIL, followed by refreshments and time for networking.

These companies have committed to staffing information tables during the networking period:

ClariFI/CapitalIQ (https://www.capitaliq.com) MathWorks (http://www.mathworks.com/index.html) There is still one table available; contact Alley Stoughton (Alley.Stoughton@gmail.com) if your company would like to claim it.

For directions to Maxwell Dworkin, see Directions to Meetup (http://www.seas.harvard.edu/our-school/map-directions) and Meetup Map (http://www.seas.harvard.edu/our-school/files/SEASCampus.pdf).

Visitor parking is available in the SEAS lot, for a fee of $5. Permits must be obtained in advance, via the Online Purchase System (https://www2.uos.harvard.edu/cgi-bin/permit/purchase.pl). Enter "School of Engineering & Applied Sciences" as the Department, and "2006" as the Department Code, when registering.

Many thanks to Greg Morrisett and Harvard University for making space available for our Meetup.

Speaker: Adam Chlipala (http://adam.chlipala.net/), MIT CSAIL

Title: Ur/Web: A Domain-Specific Functional Language for Web Applications

Abstract: Around 2006, I started working on building the ultimate programming language for modern Web applications. Today, there is an open source implementation of Ur/Web, which is starting to be used in a few non-toy projects, and I hope more will follow!

Ur/Web (http://www.impredicative.com/ur/) is inspired by languages like ML, Haskell, and Agda. There is tight integration of all aspects of Web apps; none of the many languages and protocols involved in a typical application is represented using strings, sockets, etc. Many participants will be familiar with similar approaches in languages like Links and libraries like LINQ. Ur/Web is distinguished from these by a number of novel features. First, the expressive type system allows static checking of code generators, like those popularized by Ruby on Rails scaffolding. Second, the first-class treatment of bits of Web apps is coupled with modularity features to allow true encapsulation of resources like database tables and GUI widgets. There is also an experimental static analysis for conformance to declarative security policies, which I may say a bit about, time permitting.

I plan to spend most of the time on demos of apps with source code, and this will be the most fun if everyone questions me aggressively about every feature I demonstrate. :)

P.S.: I am interested in supporting commercial development using Ur/Web. Let me know if you'd like to use it in a start-up, or if you'd be interested in doing contract work writing Ur/Web programs!

Speaker bio: Adam Chlipala (http://adam.chlipala.net/) is an assistant professor in MIT CSAIL. He finished his PhD at Berkeley in 2007. Broadly speaking, his research applies formal logic in creating better tools for producing and analyzing software. He spends a lot of time proving theorems with the Coq proof assistant, related to the verification of software infrastructure like compilers and runtime systems. He also has longstanding interests in Web programming and fancy type systems, which come together in the design of the Ur/Web language. Adam is devoting some time to commercial consulting related to real-world uses of Ur/Web.