October 2019 - talks - lists.cs.princeton.edu

Olivier Savary Belanger will present his FPO "Verified Extraction for Coq" on Thursday, 10/17/2019 at 10:30am in CS 401
by Nicki Mahler 07 Oct '19

07 Oct '19

Olivier Savary Belanger will present his FPO "Verified Extraction for Coq" on Thursday, 10/17/2019 at 10:30am in CS 401. The members of his committee are: Andrew Appel (Adviser); Examiners: Zachary Kincaid, Lennart Beringer, and Andrew Appel; Readers: David Walker and John Gregory Morrisett (Cornell University) A copy of his thesis is available upon request. Please email [ mailto:ngotsis@cs.princeton | ngotsis(a)cs.princeton ] if you would like a copy of the thesis. Everyone is invited to attend his talk. The talk abstract follows below. Interactive theorem provers allow for the development, in the same environment, of programs and of proofs about them. The programmatic portion of the development can then be extracted to code which is then compiled into an executable. However, unless both the extraction and compilation processes are formally verified, one has no guarantees that the proofs developed still apply to the resulting executable. This thesis describes my work on CertiCoq, a verified extraction pipeline for the Coq theorem prover composing with the CompCert C verified compiler to achieve end-toend correctness guarantees. I present a proof framework to prove optimizations over the continuation-passing style (CPS) intermediate representation (IR) used in CertiCoq. This framework has been used by me and others to prove the correctness of nontrivial optimizations. I focus on a novel proof of correctness for a shrink reduction algorithm, a transformation combining in a single pass multiple optimizations which always result in smaller terms. I also present a verified code generation translating the CPS IR into Clight, a front-end language of CompCert. I show how it interfaces with a verified garbage collector and how its proof composes with the proof of correctness of CompCert. Taken together, this thesis shows how carefuly crafted intermediate languages facilitate verification e↵ort in the context of an optimizing compiler.

1 0

CS Colloquium Speaker: Alexa Meade, Monday, Oct 14 at 4:30pm
by Emily C. Lawrence 07 Oct '19

07 Oct '19

CS Colloquium Speaker Alexa Meade Monday, October 14 - 4:30pm James Stewart Theater Lewis Center for the Arts, 185 Nassau Street Hosts: Adam Finkelstein & Jeff Whetstone [ https://www.cs.princeton.edu/events/25887 | https://www.cs.princeton.edu/events/25887 ] Painting in More Dimensions Artist Alexa Meade paints on the human body and three-dimensional spaces, creating the illusion that our reality is a two-dimensional painting. She will discuss her artistic process and collaborations with mathematicians, magicians, and theoretical physicists. Bio: Alexa Meade has developed a style for painting on the human body and three-dimensional spaces, creating the illusion that our reality is a two-dimensional painting. Her groundbreaking work has been exhibited around the world at the Grand Palais in Paris, the United Nations in New York, the Smithsonian National Portrait Gallery in Washington, DC and Shibuya Crossing in Tokyo. Her solo show on Rodeo Drive in Beverly Hills was attended by forty-thousand people. She has created large scale interactive installations at Coachella, Cannes Lions, and Art Basel. Alexa has been commissioned by BMW, Sony, Adidas, and the San Francisco Symphony Orchestra. She painted pop star Ariana Grande for her iconic “God is a Woman” music video, which has about 250 million views. Alexa has lectured at TED, Apple, and Stanford and accepted an invitation to the White House under President Obama. She has been honored with the "Disruptive Innovation Award" by the Tribeca Film Festival and has been Artist-in-Residence at both Google and the Perimeter Institute for Theoretical Physics. InStyle has named Alexa among their "Badass Women."

1 0

Oct 9: Maximal Mutual Information Predictive Coding for Natural Language Processing, Karl Stratos (Rutgers)
by Danqi Chen 03 Oct '19

03 Oct '19

Location: CS 402 Date: Oct 9, 2019 Time: 3-4pm Title: Maximal Mutual Information Predictive Coding for Natural Language Processing Abstract: Neural predictive coding is an enormously successful approach to unsupervised representation learning in natural language processing. In this approach, a large-scale neural language model is trained to predict the missing signal (e.g., next word, next sentence) and the trained model is used in downstream tasks to produce useful text representations. While effective, it is computationally difficult to work with and yields uninterpretable representations. In this talk, I will present a new approach to neural predictive coding based on maximal mutual information (MMI). Instead of predicting the raw missing signal, we define a set of interpretable latent "codes" and directly predict the underlying code of the missing signal. The model is trained by maximizing the mutual information between the predicted codes. I will first present a simple and effective MMI predictive coding neural model that pushes the state-of-the-art performance in unsupervised part-of-speech tagging. I will next discuss an ongoing work on generalizing MMI predictive coding to structured representations. Bio: Karl Stratos is an assistant professor in the Computer Science Department at Rutgers University. His research centers on statistical approaches to unsupervised learning in natural language processing. He completed a PhD in computer science from Columbia University in 2016. During PhD, he was advised by Michael Collins and also worked closely with Daniel Hsu. After PhD, he was a senior research scientist at Bloomberg LP (2016-2017) and a research assistant professor at Toyota Technological Institute at Chicago (2017-2019). -- *Danqi Chen* http://www.cs.princeton.edu/~danqic/

1 0

Distinguished CS Colloquium Speaker Ramón Cáceres: Wednesday, Oct 16
by Emily C. Lawrence 02 Oct '19

02 Oct '19

Distinguished CS Colloquium Speaker Ramón Cáceres from Google Wednesday, October 16 - 1:30pm Computer Science - Room 105 Host: Margaret Martonosi [ https://www.cs.princeton.edu/events/25878 | https://www.cs.princeton.edu/events/25878 ] Zanzibar: Google’s Consistent, Global Authorization System Determining whether online users are authorized to access digital objects is central to preserving privacy. This talk presents the design, implementation, and deployment of Zanzibar, a global system for storing and evaluating access control lists. Zanzibar provides a uniform data model and configuration language for expressing a wide range of access control policies from hundreds of client services at Google, including Calendar, Cloud, Drive, Maps, Photos, and YouTube. Its authorization decisions respect causal ordering of user actions and thus provide external consistency amid changes to access control lists and object contents. Zanzibar scales to trillions of access control lists and millions of authorization requests per second to support services used by billions of people. It has maintained 95th-percentile latency of less than 10 milliseconds and availability of greater than 99.999% over 3 years of production use. Bio: Ramón Cáceres is a software engineer at Google. He was previously a researcher at AT&T Labs and IBM Research. His areas of focus include computer systems and networks, mobile computing services and applications, and location data analysis and modeling. He holds a PhD in Computer Science from the University of California at Berkeley. He is an IEEE Fellow and an ACM Distinguished Scientist.

1 0

EE Lunch Seminar - Thursday, October 17, 2019, 12:30 pm, E-Quad B205 - Mohsen Imani, University of California San Diego
by Emily Lawrence 02 Oct '19

02 Oct '19

Department of Electrical Engineering Seminar Speaker: Mohsen Imani, University of California San Diego Title: Towards Learning with Brain Efficiency Date: Thursday, October 17, 2019 Time: 12:30 pm (pizza will be served) Room: E-Quad, Room B205 Host: Prof. Niraj Jha Abstract: Modern computing systems are plagued with significant issues in efficiently performing learning tasks. In this talk, I will present a new brain-inspired computing architecture. It supports a wide range of learning tasks while offering higher system efficiency than the other existing platforms. I will first focus on HyperDimensional (HD) computing, an alternative method of computation which exploits key principles of brain functionality: (i) robustness to noise/error and (ii) intertwined memory and logic. To this end, we design a new learning algorithm resilient to hardware failure. We then build the architecture exploiting emerging technologies to enable processing in memory. I will also show how we use the new architecture to accelerate other brain-like computations such as deep learning and other big data processing. Bio: Mohsen Imani is a Ph.D. candidate in the Department of Computer Science and Engineering at UC San Diego. His research interests are in brain-inspired computing and computer architecture. He is an author of more than 85 publications at top tier conferences and journals. His contributions resulted in over $40M grants funded from multiple governmental agencies (NSF, SRC) and several companies including IBM, Intel, Micron, and Qualcomm. He has received the most prestigious awards from the UCSD school of engineering including the Gordon Engineering Leadership Award and the Outstanding Graduate Research Award. He also got several nominations for the best paper awards from multiple conferences. Mohsen will be in the academic job market this year.

1 0

Oct 2: Diverse Decoding from Neural Sequence Models, Ashwin Kalyan (Georgia Tech)
by Karthik Narasimhan 01 Oct '19

01 Oct '19

Location: CS 402 Date: Oct 2, 2019 Time: 3 - 4pm Title: Diverse Decoding from Neural Sequence Models Abstract: Consider assistive technology like Google’s auto response that suggests replies with multiple intents. The ability to produce multiple diverse outputs is an integral component of such assistive systems and further, the fundamental problem of producing diverse outputs shows up across domains. In this talk, I will first introduce Diverse Beam Search (DBS) — a modification to the popular Beam Search algorithm that encourages diversity in the sequences decoded from neural sequence models. Then, I will present 𝛁BS, a fully-differentiable variant that directly models sets of sequences while optimizing more general set-level metrics including diversity. While both algorithms are task-agnostic, I will discuss their effectiveness in the context of image captioning. Bio: Ashwin Kalyan is a PhD student at Georgia Tech advised by Prof. Dhruv Batra. He is interested in developing machine learning solutions for producing diverse outputs, developing fast and accurate reasoning systems and modeling human preferences — all essential components of effective assistive technology. During his PhD, he has interned at Microsoft Research and IBM. He is also a professional violinist specializing in Karnatic Classical Music.

1 1