- 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

FW: Kurt James Werner visiting electronic music circuit modeling lecture this Wednesday, Sept 25, 5pm
by Emily Lawrence 23 Sep '19

23 Sep '19

I'm excited to let people know about a talk being presented by a visitor on Wednesday, Sept 25, at 5pm, in the PLOrk studio (Effron Music Building). Kurt James Werner will be visiting and talking about his music and giving an introduction to the techniques he uses to model analog audio circuits digitally, Wave Digital Filters (WDF). All are welcome, it's FREE and open to the public. Hope to see you there! Jeff Snyder Director of Electronic Music Princeton University --- Details below: WHEN: Wednesday, Sept 25 5pm-7pm WHERE: PLOrk Studio on the Forum Level of the Effron Music Building (in the new Lewis Arts Complex) FREE and open to the public Title: Virtual Analog Modeling using Wave Digital Filters: a Tutorial Introduction Bio: Dr. Kurt James Werner conducts research related to virtual analog (especially Wave Digital Filters), the history of music technology, 1-bit music, computer modeling of circuit-bent instruments, & sound synthesis more broadly. As part of his Ph.D. in Computer-Based Music Theory and Acoustics from Stanford University's Center for Computer Research in Music and Acoustics (CCRMA), he wrote a doctoral dissertation “Virtual Analog Modeling of Audio Circuitry Using Wave Digital Filters.” This greatly expanded the class of circuits that can be modeled using the Wave Digital Filter approach, using the classic Roland TR-808 bass drum circuit as a case study. As a researcher, he has also worked on the history of analog drum machine circuits. As a composer, his music references elements of chiptunes, musique concrète, circuit bending, algorithmic/generative composition, & breakbeat. As a Lecturer in Audio, he was based out of the Sonic Arts Research Centre (SARC) of Queen's University Belfast for several years, and will soon (in 1 week!) start a new position as a Research Engineer at iZotope, Inc. in Cambridge, MA. Synopsis: In this tutorial, the basics of the "Wave Digital Filter" (WDF) approach to virtual analog modeling will be presented. The WDF concept was introduced as a generic digital filter design technique by Alfred Fettweis in the 1970s, and has been picked up slowly by the audio DSP community starting in the early 2000s. Today, WDFs are capable of modeling audio circuits with complex topologies (bridges, feedback, &c.) and multiple nonlinearities (diodes, transistors, &c.) and can be considered one of the main approaches to modeling audio circuits in software. A wide variety of audio circuits have been successfully modeled, including the Roland TR-808 bass drum, amplifier tone stacks, Ibanez Tube Screamer, OTA-based state variable filters, tone boosters, the Electro-Harmonix Big Muff Pi, the Korg MS-50 VCF, & Fender and Mesa Boogie preamplifiers. The main focus of the talk will be the basic mathematical concepts that underpin WDF modeling and tutorial examples, including a simple RC lowpass filter & the Hammond organ vibrato/chorus circuit. Some progress on modeling a mysterious analog filter from the Experimental Music Studios (EMS) of the University of Illinois at Urbana-Champaign (UIUC) will also be presented. -- Composer, musician, instrument designer scattershot.org <http://scattershot.org> * @snyderphonics

1 0

Reminder: Colloquium Speaker Muhammad Jehangir Amjad : TODAY at 1:30pm
by Emily C. Lawrence 18 Sep '19

18 Sep '19

Colloquium Speaker Muhammad Jehangir Amjad from Google Wednesday, September 18 - 1:30pm Computer Science - Room 105 Host: Jennifer Rexford [ https://www.cs.princeton.edu/events/25874 | https://www.cs.princeton.edu/events/25874 ] Challenges in Cloud Networking Google's products, e.g. Search, YouTube, Gmail, etc. are used by billions of people the world over. Google Cloud hosts some of the most popular services in the world. Building systems that scale to support all these applications is among the greatest challenges at the company. Underlying all these systems is the network which must enable low-latency, high throughput, high capacity, high availability and secure access to compute and storage. While Google has been enormously successful in achieving these goals, cloud networking faces exciting new challenges today. With the demise of Moore's Law and explosive data growth, the implications for the performance, reliability, predictability and cost efficiency on networking, from hardware to communication protocols, will be profound. This talk will focus on highlighting some of the challenges in networking alluded to above. Additionally, we will discuss the current and future challenges in network telemetry systems and Google's approach to overcoming these challenges via statistical inference which allows us to estimate that which cannot be measured. Bio: Muhammad Jehangir Amjad is a Software Engineer in the Network Infrastructure team at Google working on inference and statistical learning on data produced by network telemetry systems. He joined Google from MIT where he has an appointment as a Lecturer of Machine Learning in CSAIL. Jehangir received his PhD from the Operations Research Center (ORC) and Laboratory of Information and Decision Systems (LIDS) at MIT, under the supervision of Prof Devavrat Shah. He received his BSE in Electrical Engineering from Princeton University.

1 0

Reminder: Colloquium Speaker Roxana Geambasu TODAY at 12:30pm
by Emily C. Lawrence 17 Sep '19

17 Sep '19

Colloquium Speaker Roxana Geambasu from Columbia University Tuesday, September 17 - 12:30pm Computer Science - Room 105 Host: Amit Levy [ https://www.cs.princeton.edu/events/25871 | https://www.cs.princeton.edu/events/25871 ] Security and Privacy Guarantees in Machine Learning with Differential Privacy Machine learning (ML) is becoming a critical foundation for how we construct the code driving our applications, cars, and life-changing financial decisions. Yet, it is often brittle and unstable, making decisions that are hard to understand and can be exploited. As one example, tiny changes to an input can cause dramatic changes in predictions; this results in decisions that surprise, appear unfair, or enable attack vectors such as adversarial examples. As another example, models trained on users' data have been shown to encode not only general trends from large datasets but also very specific, personal information from these datasets, such as social security numbers and credit card numbers from emails; this threatens to expose users' secrets through ML predictions or parameters. Over the years, researchers have proposed various approaches to address these rather distinct security, privacy, and transparency challenges. Most of the work has been best effort, which is insufficient if ML is to become a rigorous basis for how we construct our code. This talk positions differential privacy (DP) -- a theory developed by the privacy community -- as a versatile foundation for building into ML much-needed guarantees of not only privacy but also of security, stability, and transparency. As supporting evidence, I first present PixelDP , a scalable certified defense against adversarial examples that leverages DP theory to guarantee a level of robustness against this attack. I then present Sage, a DP ML platform that bounds the leakage of personal secrets through ML models while addressing some of the most pressing challenges of DP, such as the "running out of privacy budget" problem. Both PixelDP and Sage are designed from a pragmatic systems perspective and illustrate that DP theory is powerful but requires adaptation to achieve practical guarantees for ML workloads. Bio: Roxana Geambasu is an Associate Professor of Computer Science at Columbia University and a member of Columbia's Data Sciences Institute. She joined Columbia in Fall 2011 after finishing her Ph.D. at the University of Washington. For her work in cloud and mobile data privacy, she received: an Alfred P. Sloan Faculty Fellowship, an NSF CAREER award, a Microsoft Research Faculty Fellowship, several Google Faculty awards, a "Brilliant 10" Popular Science nomination, the Honorable Mention for the 2013 inaugural Dennis M. Ritchie Doctoral Dissertation Award, a William Chan Dissertation Award, two best paper awards at top systems conferences, and the first Google Ph.D. Fellowship in Cloud Computing.

1 0

Colloquium Speaker Muhammad Jehangir Amjad : Wednesday, Sept. 18
by Emily C. Lawrence 11 Sep '19

11 Sep '19

Colloquium Speaker Muhammad Jehangir Amjad from Google Wednesday, September 18 - 1:30pm Computer Science - Room 105 Host: Jennifer Rexford [ https://www.cs.princeton.edu/events/25874 | https://www.cs.princeton.edu/events/25874 ] Challenges in Cloud Networking Google's products, e.g. Search, YouTube, Gmail, etc. are used by billions of people the world over. Google Cloud hosts some of the most popular services in the world. Building systems that scale to support all these applications is among the greatest challenges at the company. Underlying all these systems is the network which must enable low-latency, high throughput, high capacity, high availability and secure access to compute and storage. While Google has been enormously successful in achieving these goals, cloud networking faces exciting new challenges today. With the demise of Moore's Law and explosive data growth, the implications for the performance, reliability, predictability and cost efficiency on networking, from hardware to communication protocols, will be profound. This talk will focus on highlighting some of the challenges in networking alluded to above. Additionally, we will discuss the current and future challenges in network telemetry systems and Google's approach to overcoming these challenges via statistical inference which allows us to estimate that which cannot be measured. Bio: Muhammad Jehangir Amjad is a Software Engineer in the Network Infrastructure team at Google working on inference and statistical learning on data produced by network telemetry systems. He joined Google from MIT where he has an appointment as a Lecturer of Machine Learning in CSAIL. Jehangir received his PhD from the Operations Research Center (ORC) and Laboratory of Information and Decision Systems (LIDS) at MIT, under the supervision of Prof Devavrat Shah. He received his BSE in Electrical Engineering from Princeton University.

1 0