Powered by
21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016),
September 18–24, 2016,
Nara, Japan
Invited Talks
TensorFlow: Learning Functions at Scale
Martín Abadi
(Google, USA)
TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. Its computational model is based on dataflow graphs with mutable state. Graph nodes may be mapped to different machines in a cluster, and within each machine to CPUs, GPUs, and other devices. TensorFlow supports a variety of applications, but it particularly targets training and inference with deep neural networks. It serves as a platform for research and for deploying machine learning systems across many areas, such as speech recognition, computer vision, robotics, information retrieval, and natural language processing.
In this talk, we describe TensorFlow and outline some of its applications. We also discuss the question of what TensorFlow and deep learning may have to do with functional programming. Although TensorFlow is not purely functional, many of its uses are concerned with optimizing functions (during training), then with applying those functions (during inference). These functions are defined as compositions of simple primitives (as is common in functional programming), with internal data representations that are learned rather than manually designed.
TensorFlow is joint work with many other people in the Google Brain team and elsewhere. More information is available at tensorflow.org.
@InProceedings{ICFP16p1,
author = {Martín Abadi},
title = {TensorFlow: Learning Functions at Scale},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {1--1},
doi = {},
year = {2016},
}
Journey to Find Bugs in JavaScript Web Applications in the Wild
Sukyoung Ryu
(KAIST, South Korea)
Analyzing real-world JavaScript web applications is a challenging task. On top of understanding the semantics of JavaScript, it requires modeling of web documents, platform objects, and interactions between them. Not only the JavaScript language itself but also its usage patterns are extremely dynamic. JavaScript can generate code and run it during evaluation, and most web applications load JavaScript code dynamically. Such dynamic characteristics of JavaScript web applications make pure static analysis approaches inapplicable.
In this talk, we present our attempts to analyze JavaScript web applications in the wild mostly statically using various approaches. From pure JavaScript programs to JavaScript web applications using platform-specific libraries and dynamic code loading, we explain technical challenges in analyzing each of them and how we built an open-source analysis framework for JavaScript, SAFE, that addresses the challenges incrementally.
In spite of active research accomplishments in analysis of JavaScript web applications, many issues still remain to be resolved such as events, callback functions, and hybrid web applications. We discuss possible future research directions and open challenges.
@InProceedings{ICFP16p2,
author = {Sukyoung Ryu},
title = {Journey to Find Bugs in JavaScript Web Applications in the Wild},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {2--2},
doi = {},
year = {2016},
}
A Functional Programmer's Guide to Homotopy Type Theory
Dan Licata
(Wesleyan University, USA)
Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical disciplines of homotopy theory and higher-dimensional category theory. From a programming point of view, these connections have revealed that all types in dependent type theory support a certain generic program that had not previously been exploited. Specifically, each type can be equipped with computationally relevant witnesses of equality of elements of that type, and all types support a generic program that transports elements along these equalities. One mechanism for equipping types with non-trivial witnesses of equality is Voevodsky’s univalence axiom, which implies that equality of types themselves is witnessed by type isomorphism. Another is higher inductive types, an extended datatype schema that allows identifications between different datatype constructors. While these new mechanisms were originally formulated as axiomatic extensions of type theory, recent work has investigated their computational meaning, leading to the development of new programming languages that better support them. In this talk, I will illustrate what univalence and higher inductive types mean in programming terms. I will also discuss how studying some related semantic settings can reveal additional structure on types; for example, moving from groupoids (categories where all maps are invertible) to general categories yields an account of coercions instead of equalities. Overall, I hope to convey some of the beauty and richness of these connections between disciplines, which we are just beginning to understand.
@InProceedings{ICFP16p3,
author = {Dan Licata},
title = {A Functional Programmer's Guide to Homotopy Type Theory},
booktitle = {Proc.\ ICFP},
publisher = {ACM},
pages = {3--3},
doi = {},
year = {2016},
}
proc time: 1.01