The Boston chapter of Papers We Love
What was the last paper within the realm of computing you read and loved? What did it inspire you to build or tinker with? Come share the ideas in an awesome academic/research paper with fellow engineers, programmers, and paper-readers. Lead a session and show off code that you wrote that implements these ideas or just give us the lowdown about the paper. Otherwise, just come, listen, and discuss in a low ego, friendly environment.
Papers We Love has a Code of Conduct. Please contact one of the Meetup's organizers if anyone is not following it. Be good to each other and to the PWL community!
Sign-up: Please RSVP for meetings via Meetup.com
Niko Matsakis, one of the core Rust contributors, is going to present some proof techniques from Prolog that are informing some advanced work in Rust's type checker and compiler.
Traditional Prolog lets you define logical relationships and then have the solver figure out the inferences. But Prolog's Horn Clauses are fairly simplistic in terms of what they can express. This paper talks about a few relatively simple techniques that lets us extend to a much richer logic, supporting things like proving that one statement implies another, or proving "for all" predicates. So for example where Prolog could perhaps setup rules to decide when `hungry(joe)` is true or `hungry(nancy)`, this technique describes techniques to prove `hungry(P)` is true for *any* person P.
"A proof procedure for the logic of hereditary Harrop formulas", Gopalan Nadathur, Journal of Automated Reasoning, Feb 1993, 11(1), pp[masked].
We're very excited to have Heather Miller reprise her PWLConf talk!
Nowadays, most programs we write are in some sense distributed—making HTTP requests or serving responses over HTTP, fetching or computing data on some remote resource, building some microservice that is meant to interact with others, etc. With all of this distribution going on, one might ask, what happened to distributed programming languages? Why are we still using languages like Java or C++ for these sorts of tasks? In this talk, Heather will take us on a whirlwind tour through history up to the present of distributed programming languages as well as programming constructs meant for distribution like futures and RPC. Together, we'll try to work out what happened to all of the distributed programming languages!
References Programming Models for Distributed Comp…
Join us as Chelsea Voss presents a handful of papers on DNA computing:
• Leonard Adleman (the "A" in RSA). Computing with DNA.
• Faulhammer et al. Molecular computation: RNA solutions to chess problems.
• Qian + Winfree's Strand displacement circuits
• Rothemund + Winfree + Papadakis, Algorithmic Self-Assembly of DNA Sierpinski Triangles – "DNA origami" implementing cellular automata…
Join us for some programming language pragmatics! Joe Jevnik will present Simon Peyton Jone's "Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine".
The Spineless Tagless G-machine is an abstract machine designed to support nonstrict higher-order functional languages. This presentation of the machine falls into three parts. Firstly, we give a general discussion of the design issues involved in implementing non-strict functional languages.
Next, we present the STG language, an austere but recognisably-functional language, which as well as a denotational meaning has a well-defi ned operational semantics. The STG language is the "abstract machine code" for the Spineless Tagless G-machine.
Lastly, we discuss the mapping of the STG language onto stock hardware. The success o…
Godel's Incompleteness Theorems are among the most famous results in modern mathematics. They are often informally stated as follows:
1. Any formal system that can express elementary arithmetic contains statements that are "true but not provable".
2. Any consistent formal system that can express elementary arithmetic cannot prove its own consistency.
These informal statements, however, often raise more questions than they answer. What exactly is a "formal system"? What does it mean for a statement to be "true but not provable"? What does it mean to "express arithmetic", and why does arithmetic have anything to do with proof or consistency?
This talk will introduce the audience to the main ideas behind the incompleteness theorems. We'll discuss the historical context in which the incompleteness theorems were discovered, develop the concepts necessary to properly understand what the theorems actually say, and present a sketch of the theorems' proof.…
"You are not expected to understand this." That is the now famous comment in UNIX v6's process switching (swtch) code. Process switching -- and multitasking more generally -- is a neat magic trick the OS pulls off. It's a delicate dance between the operating system and the hardware. We will dig into how this dance works on UNIX v6 and the PDP11, including the famous comment. We will also look into how the process switching magic happens on a more recent OS and CPU architecture (FreeBSD on x86). It should be a fun trip down the rabbit hole of operating system kernels internals and instruction set specifications…
An oversimplified history of CSP
Communicating Sequential Processes (CSP) was first described by Tony Hoare in 1978. Since then, there have been two main "branches" of further development. In the first branch, CSP inspired how concurrency is handled in an ongoing series of programming languages — most recently (and famously) in Go. In the second branch, CSP was refined into a rigorous "process calculus", and has since been used to formally prove various safety and liveness properties of concurrent and distributed systems.
This talk will be a whirlwind history of CSP, a high-level overview of the process calculus, and some live demos of using a refinement checker to prove things about interesting systems. (No proving things by hand!)
CAR Hoare. "Communicating Sequential Processes", CACM 21(8), pp. [masked], 1978.
CAR Hoare. Communi…
Have you ever wished GUI tools for building visuals like PowerPoint and Illustrator had a more programming-like interface for making similar images rather than copying, pasting, and tweaking all the time? Have you ever wished programmatic systems like LaTeX and Processing.js allowed you to just click and drag on items in the output to change the result, rather than going through an edit-compile-run cycle every time? In some of the latest research, you can have both!
In this talk, Jon Schuster will discuss "Programmatic and Direct Manipulation, Together at Last"  from this year's PLDI (Conference on Programming Language Design and Implementation). The paper proposes a method to automatically edit an SVG-generating program to match the changes made by dragging components of the resulting image around the canvas, while still allowing the developer to edit the code directly. A prototype is available online , so expect interactive demos!
A shorter position paper  t…
Tim Riser on Mastering the Game of Go with Deep Neural Networks & Tree Search
A grand challenge of AI has fallen - a decade earlier than the ever-abused experts predicted. But should we care?
What made AlphaGo, the AI built by DeepMind, so unique?
To dive into AlphaGo's system of learning, evaluation, and search algorithms that combined to defeat the reigning Go world champion, Tim will be presenting on "Mastering the Game of Go with Deep Neural Networks & Tree Search", a paper by Google DeepMind.
Tim Riser is currently researching at the Berkman Center for Internet & Society at Harvard University. He graduated from Brigham Young University wit…
What we gonna do right now is go back.
How far back?
Intro- You probably know that many influential technologies were developed by Xerox: Ethernet, networking protocols, bitmapped workstations, laser printing technology and object oriented programing, etc.
So brush up on your OSI model and be ready to dive into networking archeology. Come here the story of XNS, which became the canonical protocol in early days of local area networking.
XNS greatly influenced protocols such as Novell NetWare, and Banyan VINES, AppleTalk and lives on within the corners of the Internet. https://goo.gl/Ev3atn
Steven Willis is an engineer, executive and co-founder of networking companies such as Wellfleet and Argon. From 1982 to 1986, he worked as a developer at Interlan, one of the original Ethernet controller companies, developing …
History! Those who don't know it are doomed to etc.
Smalltalk is one of the earliest object-oriented languages. It's extremely influential — many of the OO concepts that we use in today's languages were first developed in Smalltalk. But what influenced Smalltalk? Alan Kay will walk us through the language's inspirations in this talk, including such crazy new technologies as UIs with overlapping windows and a 1970's-era ur-tablet!
Douglas Creager is a software engineer at Google with an eclectic history. He got a CS Master's from MIT working in a biology group, and a PhD from Oxford while teaching formal methods to professional software engineers. He's worked as a consultant helping finance and telecoms firms wrangle data between different systems, and was VP of Engineering for a network security startup based out of DC. He liv…
PWL Boston / Cambridge
We are thrilled to have Peter Bailis as the speaker for our April meeting. Peter is brilliant researcher and outstanding speaker. He will be presenting on Streaming Queries over Streaming Data" from VLDB 2002 by Sirish Chandrasekaran and Michael J. Franklin.
After spending this year visiting MIT CSAIL, Peter Bailis will join Stanford Computer Science as an assistant professor. Peter's research in the Future Data Systems group (http://futuredata.stanford.edu) focuses on the design and…
PWL Boston / Cambridge is back!
Ripped from the headlines, but not Law and Order, Richard Littauer will be presenting on "The Moral Character of Cryptographic Work" by Phillip Rogaway of UC Davis.
"Richard Littauer is a computer scientist and developer who lives in Cambridge. He works for IPFS (ipfs.io), building a distributed, permanent internet, and reads papers and books in his constantly dwindling spare time. He's most well known for writing the dictionary for the Na'vi language, and for getting paid to review websites while drunk at theuserisdrunk.com."
PWL Boston / Cambridge is hosted at the Battery Ventures office in the Seaport:
One Marina Park Drive, FL 11
Boston, MA 02210
Upon arriving at One Marina Park Drive, you will need your IDs to check in…