Wednesday, March 26, 2014

01:30 pm
- 02:30 pm

Computer Science Seminar, Danny Krizanc (Wes): "Mobile Agent Rendezvous"

Abstract:<br/><br/>Alpern (1976) is credited with asking the following question:<br/>Two astronauts land on a large spherical body. The body has no fixed orientation in space, no axis of rotation, so that no common notion of position or direction is available to the astronauts. Given unit walking speeds how should they move about so as to minimize the expected time until they meet?<br/><br/>This has lead to a great deal of research on so-called "rendezvous" problems. This talk will survey a small portion of this research as it has developed in the study of mobile agents.<br/>

ESC 618

Wednesday, February 26, 2014

01:30 pm
- 02:30 pm

Computer Science Seminar, Henny Admoni (BA'08 MA'09, Yale University): "The Role of Eye Gaze in Social Robotics"

Abstract: Eye gaze is an important component of human social interaction, and is therefore a key element in the design of robots that interact in social environments with people. Experiments investigating eye gaze in human-robot interactions have shown that robot gaze is often interpreted in similar ways to human gaze, facilitating efficient non-verbal communication between robots and humans. However, on a cognitive level, robot gaze fails to cue reflexive human attention, indicating that some difference exists between how people process eye gaze from humans and from robots. My research focuses on modeling human gaze behavior and understanding how these models differ when applied to robots. This research has applications in a variety of areas that involve robots interacting with people, particularly for socially assistive robots.<br/><br/>Bio:<br/>Henny Admoni (BA '08 MA '09) is a PhD candidate and a member of the Social Robotics Laboratory in the Department of Computer Science at Yale University, where she is advised by Professor Brian Scassellati. Henny creates and studies robots that interact closely with people, and her research is about how to leverage non-verbal social cues, such as eye gaze, to make these human-robot interactions more effective. More information can be found at http://hennyadmoni.com.<br/>

ESC 618

Tuesday, February 11, 2014

04:15 pm
- 05:30 pm

CS Seminar, Ran Libeskind-Hadas (Harvey Mudd College): "The Hitchhikers Guide to Coevolution"

Abstract: In the "Origin of Species," Darwin speculated that the evolution of one species could effect the evolution of another. For example, bees and flowers might have coevolved in a mutually beneficial way. In other cases, a parasitic species might track the evolutionary history, or "hitchhike", on its host species. In recent years, computational methods have been developed that allow biologists to study if and how pairs of species might have coevolved. In this talk, I will describe the computational problems, algorithmic solutions, and the resulting software systems that have been developed to study coevolution, offering several examples of how these computational tools have led to interesting discoveries.<br/><br/>Bio: Ran "RON" Libeskind-Hadas is the R. Michael Shanahan Professor of Computer Science at Harvey Mudd College. He received the A.B. in applied mathematics at Harvard University and the M.S. and Ph.D. in computer science at the University of Illinois at Urbana-Champaign. His research interests are in algorithms and computational biology. <br/>

ESC 638

Tuesday, November 19, 2013

12:00 pm
- 01:00 pm

Computer Science Seminar: Howard Blair, Syracuse University

Abstract: The relatively recent developments that exploit quantum phenomena for computing faster and communicating more securely have re-energized research into the basics of quantum phenomena and are forcing researchers to confront the problem of explaining how the world can actually be the way we observe it to be: The world is quantum mechanical.<br/><br/>The talk will present an overview of:<br/> * Qubits(quantum bits)<br/> * Quantum registers<br/> * Quantum state transitions<br/>and will review several well-known results that argue for the nonexistence of definite quantum states until a measurement is made.<br/>The talk will also sketch Abramskya'™s simple imperative quantum programming language as a practical tool for prototyping code for quantum algorithms, with consequences for proving quantum programs correct and for algorithm complexity.<br/><br/>"€œAnyone who is not shocked by quantum theory has not understood it."<br/> -€“Niels Bohr<br/><br/>Prof. Blair teaches undergraduate and graduate courses in quantum computing in the Department of Electrical Engineering and Computer Science at Syracuse University. He conducts research in software and hardware verification and validation of classical and quantum computing systems as well as hybrid discrete/continuous dynamical systems. In these endeavors he collaborates with computer scientists, mathematicians, biologists, physicists and philosophers at Syracuse University and other universities and at the U.S Air Force Research Laboratory in Rome, NY.<br/>

ESC 638

Tuesday, November 12, 2013

04:15 pm
- 05:30 pm

Computer Science Seminar: Richard Silverman (D.E. Shaw)

Title: Basics of IP routing: Distance-vector vs. link-state approaches<br/><br/>When you launch a packet of data onto the Internet, how does it get where it's going? At each hop along the path to its destination, a network device called a router forwards the packet along, but how does each router know the best way to send a given packet to any of several billion possible addresses? Does each router have a complete map of the Internet? If not, how can it make these decisions? And, what happens if the network changes: if a path stops working, or a new one becomes available?<br/><br/>To deal with these issues, we have dynamic routing protocols: mechanisms which allow routers to discover each other, find and maintain optimal paths to all reachable destinations, deal with link failures and additions, and more. In this talk, we will focus on the class of interior gateway protocols, and discuss the two dominant approaches to routing: distance-vector and link-state algorithms, as embodied in the RIP and OSPF routing protocols.<br/><br/>Since earning his B.A. in computer science and M.A. in pure mathematics, both at Wesleyan University, Richard Silverman has worked in the fields of networking, formal methods in software development, computer security, and Unix systems administration. He has co-authored two books on computer security published by O'Reilly: SSH, The Secure Shell (The Definitive Guide), and the Linux Security Cookbook. He is currently on the engineering staff of D. E. Shaw & Co., L.P., a company focused on areas it believes can be fundamentally altered by the application of computing technology -- in fields ranging from finance to molecular biology.

ESC 638

Tuesday, October 29, 2013

04:15 pm
- 05:30 pm

Computer Science Seminar: Arjun Guha (UMass Amherst)

Title: Reclaiming security for web programmers<br/><br/>Abstract: The Web enables new classes of programs that pose new security<br/>risks. For example, because Web programs freely mix data and code from<br/>untrusted sources, major websites have been compromised by third-party<br/>components, such as malicious ads. In addition, users cannot fully<br/>control which programs run; Web programs are visited, not installed.<br/>Therefore, Web security is entirely in the hands of programmers, not<br/>users.<br/><br/>I address the problem of securing existing Web programs, which are<br/>universally written in JavaScript. Unfortunately, JavaScript has<br/>several warts that make it difficult to reason about even simple<br/>snippets of code. Several companies have developed "Web sandboxes" to<br/>make JavaScript programming safe. However, these Web sandboxes have no<br/>security guarantees.<br/><br/>In this talk, I show how programing languages research can be used to<br/>verify properties of Web applications. I present a type-based<br/>verification method for JavaScript that we use to find bugs in and<br/>produce the first verification of an existing, third-party Web sandbox.<br/><br/>Programming language techniques can give us mathematical proofs of<br/>security, but attackers attack implementations, not theorems. I discuss<br/>our approach to doing principled, real-world Web security research,<br/>which combines semantics with systems. I also review additional projects<br/>that use our tools and techniques.<br/><br/><br/>Bio: Arjun Guha is an assistant professor of Computer Science at UMass<br/>Amherst. He enjoys tackling practical problems, while adhering to the<br/>mathematical foundations of programming languages. For example, his<br/>dissertation on JavaScript semantics and type-checking, from Brown<br/>University, is used by several other researchers as a foundation for<br/>their own work. As a postdoc at Cornell University, he developed a model<br/>of software-defined networking (SDN) in the Coq Proof Assistant, which<br/>is the foundation for a verified runtime and other SDN tools. His<br/>research has led to several software systems, such as LambdaJS,<br/>Frenetic, and Flapjax that are in active use.<br/>

ESC 638

Friday, October 11, 2013

01:15 pm
- 02:15 pm

Computer Science Seminar: Jim Royer (Syracuse University)

Abstract: We investigate the notion of feasible computability over<br/>inductive structures (henceforth, data) and coinductive structures<br/>(henceforth, codata). Data includes: natural numbers, strings of<br/>characters, (finite) lists, (finite) trees, etc. Codata includes:<br/>various sorts of potentially infinite lists (streams) and potentially<br/>infinite trees. We also investigate simple typed programming formalisms<br/>that attempt to capture feasible computability over data and codata.<br/><br/>Pinning down ``feasible computability'' over data and codata and<br/>capturing it in a programming formalisms turn out to be a subtle problem<br/>for which there is not yet a final answer. The present work focuses on<br/>bettering our understanding these problems and crafting tools to deal<br/>with them.<br/><br/>We start by introducing some simple classical systems for computing over<br/>data (via structural recursions) and codata (via structural<br/>corecursions) whose computational power goes well beyond the feasible.<br/>We rein in these systems by imposing a simple, two level ramification of<br/>their types (based on Bellantoni and Cook's normal/safe distinction).<br/>The resulting systems are nice and simple and a little surprising in<br/>what they compute and what they seem to fail to compute, especially in<br/>the codata realm.<br/><br/>The talk will be a tour through these various systems, focusing on<br/>motivations, definitions, examples, counterexamples, and open problems<br/>that our work reveals.<br/><br/>This is joint work with Norman Danner (Wesleyan University).

ESC 638

Tuesday, October 01, 2013

04:15 pm
- 05:30 pm

Computer Science Seminar, Norman Danner (Wesleyan): Simulating (parts of) the Tor Network

Tor is probably the most widely-used anonymity network today. Because many people use it, new protocols cannot be tested on the deployed network, which makes it difficult to understand impacts and effects of proposed changes. This also affects our ability to understand possible attack vectors and defenses. Modeling and simulation of the network is therefore crucial. However, much research relies on simple models of both users and the network itself. I will discuss recent (and not so recent) investigations into more sophisticated simulation techniques, focusing on simulation of user behavior with hidden Markov models. I will in part be channeling Julian Applebaum '13, whose thesis contains much of this work.

ESC 638

Tuesday, April 09, 2013

04:30 pm
- 05:30 pm

Computer Science Seminar, Kegan Samuel: "How do computers 'see'?"

Abstract: The human visual system can perceive and understand the world around with apparently very little difficulty. In the computer vision field, researchers attempt process and understand digital representation of images in a similar manner using various computer algorithms or mathematical models. While much has been accomplished in the field, there is still a significant amount of work to be done before a system is developed which would be able to interpret images at a level close to that of humans. <br/><br/>In addition to a brief overview of the problems encountered in the field of computer vision, I will also speak on work dealing with the use of Markov Random Field(MRF) models applied to the tasks of denoising and image segmentation. <br/>

ESC 638

Tuesday, May 01, 2012

04:15 pm
- 05:30 pm

Computer Science Seminar, Stefan Sundseth '13: The Pi-Calculus for Mobile Systems

Abstract: In today's world computation revolves around interaction between multiple systems, yet the most well-known models of these computational systems neglect their ability to communicate with external processes. <br/>The Pi-Calculus was created as a means to rigorously describe a model whose fundamental action is to send and receive messages across an interface, which means that multiple processes can be synchronized by concurrent send/receive directives. Though simple, the Pi-Calculus is actually quite powerful as concepts such as algorithms, object-oriented programming, and the lambda-calculus fall within its scope.<br/>

ESC 339

Tuesday, April 24, 2012

04:15 pm
- 05:30 pm

Computer Science Senior Thesis Talks: Jennifer Payking, Jeffrey Ruberg and Micah Wylde

Abstracts:<br/><br/>Jennifer Paykin: Automated Cost Analysis of a Higher-Order Language in Coq<br/><br/>The cost analysis of a program is a function from the size of its input to the number of steps the program takes to run. In this work we address two difficulties associated with constructing cost analyses. First, what is the cost of a higher-order program? If an expression takes a function as input, what is the size of that input? If an expression evaluates to a function, what is its cost? Second, how can we automate the cost analysis of arbitrary programs?<br/>In this work we develop a static cost analysis system for a functional target language with structural list recursion. A translation function maps target expressions e to complexities encoding upper bounds on both the cost of evaluating e and some measure of e's size. We implement the translation in the proof assistant Coq, formally verifying the soundness of the translation scheme. The resulting system generates certified upper bounds on the complexity of target language terms.<br/><br/><br/>Jeffrey Ruberg: Charming a Python with Static Type Checking<br/><br/>Pyty is a static typechecker for the Python programming language. Pyty imposes a static type system on users, for which they provide type declarations via comments. The type system developed is modeled on the Hindley-Milner type inference algorithm for the lambda calculus and its application to ML. Much of the implementation challenge is in applying this type system to a language not designed with typechecking in mind. <br/>The type system describes a system of deriving type assignments, whereby we can prove that a Python term can be assigned a specific type; we do this by searching for a valid tree of type assignment rules. Pyty also employs type inference for a restricted subset of the Python language in order to facilitate the typechecking algorithm.<br/><br/>Micah Wylde: Safe Motion Planning for Autonomous Driving<br/><br/>Self-driving cars have the potential to revolutionize transportation by making it cheaper, safer and more efficient. In this work we describe a novel motion planning system for translating high-level navigation goals into low-level actions for controlling a car. Specifically, the motion planning system is responsible for choosing at each time step an appropriate velocity and steering angle, which could then be implemented by the driving hardware or simulation. Our planner is able to compute a safe and efficient trajectory in a dynamic environment while staying within its lane and avoiding obstacles.<br/>

ESC 339

Tuesday, February 28, 2012

04:15 pm
- 05:15 pm

Computer Science Seminar, Matt Eaton '04, Computer Science and Artificial Intetelligence Lab, MIT: "Chromatin and epigenetic regulation in DNA replication and Alzheimer's disease"

Abstract: In the nucleus of every eukaryotic organism, DNA is compacted and organized by wrapping around histone proteins in a structure called chromatin. Chromatin is a dynamic structure, and encoded in the histone tails are chemical modifications that provide clues to the underlying regulation of DNA-templated processes such as RNA transcription and DNA replication. This "histone code" can be measured genome-wide with high-throughput assays such as ChIP-sequencing.<br/><br/>A further layer of information is encoded in chemical modifications to the DNA itself; for example, cytosine residues in the genomes of higher eukaryotes can be methylated by nuclear proteins in heritable fashion, and this methylation can alter gene expression.<br/>Taken together, these layers of information encoded on top of the DNA sequence make up a large part of the field of epigenetics: the study of heritable, non-sequence, cis-acting changes to nuclear DNA and chromatin.<br/><br/>In this talk, I will give three examples of how machine learning and computer science techniques were used to help elucidate the epigenetic landscape in both model organisms and human disease. The first will examine the role of nucleosome positioning around origins of DNA replication in the genome of the budding yeast, Saccharomyces cerevisiae. The second example examines the role of the histone code in specifying the replication program of the fruit fly Drosophila melanogaster. Finally, I will discuss ongoing work in examining the role of DNA methylation in the cognitive decline of Alzheimer's disease patients.<br/>

ESC 113

Thursday, February 23, 2012

12:00 pm
- 01:00 pm

(Computer Science Seminar) Matt Ginsberg, CEO On Time Systems, Inc: "Dr. Fill: Crosswords and An Implemented Solver for Singly Weighted CSPs"

Abstract: We describe and demonstrate Dr.Fill, a program that solves American-style crossword puzzles. From a technical perspective, Dr.Fill works by converting crosswords to weighted constraint satisfaction problems (CSPs), and then using a variety of novel techniques to find a solution. These techniques include generally applicable heuristics for variable and value selection, a variant of limited discrepancy search, and postprocessing and partitioning ideas. Branch and bound is not used, as it was incompatible with postprocessing and was determined experimentally to be of little practical value. Dr.Filll's performance on crosswords from the American Crossword Puzzle Tournament suggests that it ranks among the top fifty or so crossword solvers in the world.

ESC 339

Wednesday, November 30, 2011

04:15 pm
- 06:00 pm

Dan Dougherty, Wes and Worcester Polytechnic Institute: Symbolic protocol analysis for implicitly authenticated Diffie-Hellman

Abstract:<br/><br/>Joint work with Joshua Guttman, WPI.<br/><br/>We develop new techniques for rigorous symbolic proofs of security<br/>properties for implicitly authenticated Diffie-Hellman protocols. These<br/>protocols, e.g.~{MQV} and the Unified Model, which construct a shared<br/>secret using a minimum of communication, have been challenging both for<br/>symbolic and computational analyses. Their essential use of rich<br/>algebraic structure has been an obstacle.<br/><br/>We prove implicit authentication and secrecy results for several<br/>protocols in this group. The same methods yield proofs of forward<br/>secrecy, for protocols where it holds, and indicate why it does not<br/>otherwise. Resistance to compromised key attacks and impersonation<br/>attacks may be resolved similarly.<br/><br/>Our crucial notion is the \emph{indicator}, a vector of integers that<br/>summarizes how many times each secret exponent appears in a message. We<br/>prove that the adversary can never construct a message with a new<br/>indicator in our adversary model.<br/><br/>Although we work with a message algebra generated by the normal forms<br/>for an equational theory $AG^$, we also give a model-theoretic proof<br/>that $AG^$ faithfully reflects all equations that are true uniformly as<br/>the prime $q$ varies. Hence, our security theorems ensure that the<br/>adversary has no strategy that is expressible algebraically and works<br/>uniformly---independent of the choice of $q$---for producing a<br/>counterexample. Computational soundness awaits further investigation.<br/>

ESC 638

Tuesday, November 01, 2011

04:15 pm
- 05:30 pm

Comp Seminar: Summarizing the News

Speaker: Dan Gillick, '03, UC Berkeley and Google<br/><br/>Abstract: The goal of automatic summarization is to generate a short summary of a document, or a set of related documents. This is hard for people, let alone computers. I'll describe how these systems work, how they are evaluated, and how I improved them. Hopefully, there will be a demo.

ESC 339

Tuesday, October 18, 2011

04:15 pm
- 05:30 pm

Computer Science Seminar: Abstract notions of computation and monads Part 2

Speaker: Emilio Jesus Gallego Arias, UPM Madrid and Wesleyan University<br/><br/>Abstract: Every day, thousands of programmers alien to category theory use monads as a fundamental tool to their work. In fact, in popular functional languages like Haskell you cannot write a program without using a monad.<br/><br/>At the time monads were first studied in the context of category theory, computer science didn't have a need for them. 20 years after that, a new kind of functional programming languages was born, advocating the usage of Scott's computable functions as the main primitive for program construction.<br/><br/>Semantics based on mathematical functions have numerous advantages, but essential needs such as input/output, global state, error handling, etc... couldn't be solved in an elegant way due to the lack of side effects and order or evaluation issues.<br/><br/>We will start with categorical semantics for functional programming and monads understood as a "notion of computation". This allows otherwise impure or ugly constructions. We will discuss the evolution of monads, from the first theoretical papers to real world use and implementation.<br/><br/>We will focus on how the original notion led to an "abstract notion of computation" or "abstract computation types", akin to the popular "abstract data types" paradigm. Last, we will present joint work with Prof. Lipton about incorporating the notion of "abstract computation" to logic programming.<br/>

ESC 339

Thursday, October 06, 2011

11:30 am
- 02:00 pm

WANTED! CS Majors to Study Abroad

Speaker: Dr. Andras Recski, Director of Academic Programs, AIT BUDAPEST<br/><br/>An upcoming talk will be presented on campus to encourage students to consider a great new study abroad program, Aquincum Institute of Technology BUDAPEST, for students interested in computing, design, computational biology, and IT entrepreneurship.<br/><br/>Andras Recski, Director of Academic Programs at AIT, will be giving a presentation about the program on THURSDAY, OCTOBER 6, 2011 including a NOON LUNCH. Pizza and treats from Hungary will be served!<br/><br/>About AIT: The AIT program has a first-rate faculty including professors such as Erno Rubik (inventor of the Rubik's Cube and recent recipient of the U.S. Outstanding Contributions to Science Education Award), an innovative curriculum including courses such as "Computer Vision for Digital Film Post-production" taught by faculty affiliates from Colorfront Studios (recent recipients of an Academy Award for technical contributions), and a guest lecture series that brings prominent speakers to campus.<br/><br/>All classes are conducted in English at AIT's state-of-the-art campus on the lovely banks of the Danube River. Students live in vibrant neighborhoods of Budapest and have ample opportunities to interact with Hungarian students and explore Hungary and the region.<br/><br/>AIT is small and friendly, with typical class sizes of 5-15 students.<br/>Recent U.S. AIT students have come from Franklin W. Olin College of Engineering, Harvey Mudd College, Northeastern University, Pomona College, Princeton University, RPI, Skidmore, Smith, Swarthmore and Williams Colleges. The program also includes a small number of Hungarian students. AIT Alumni site: http://www.ait-budapest.com/ait-alumni<br/><br/>The AIT website and APPLICATION materials are available on-line at:<br/>http://www.ait-budapest.com<br/><br/>Applications for the Spring 2012 term are due by November 15, 2011.<br/>(Although, completed submissions are currently being accepted and reviewed. Notice is then given within two weeks time.)<br/><br/>Contacts: Prof. Ran Libeskind-Hadas (hadas@cs.hmc.edu) and Prof. Michael Orrison (orrison@math.hmc.edu) at Harvey Mudd College are serving as the North American Co-Directors for AIT, and are eager to answer any questions that you might have.<br/>

ESC 184 (Woodhead Lounge)

Tuesday, October 04, 2011

04:15 pm
- 05:30 pm

Abstract notions of computation and monads

Speaker: Emilio Jesus Gallego Arias, UPM Madrid and Wesleyan University<br/><br/>Abstract: Every day, thousands of programmers alien to category theory use monads as a fundamental tool to their work. In fact, in popular functional languages like Haskell you cannot write a program without using a monad.<br/><br/>At the time monads were first studied in the context of category theory, computer science didn't have a need for them. 20 years after that, a new kind of functional programming languages was born, advocating the usage of Scott's computable functions as the main primitive for program construction.<br/><br/>Semantics based on mathematical functions have numerous advantages, but essential needs such as input/output, global state, error handling, etc... couldn't be solved in an elegant way due to the lack of side effects and order or evaluation issues.<br/><br/>We will start with categorical semantics for functional programming and monads understood as a "notion of computation". This allows otherwise impure or ugly constructions. We will discuss the evolution of monads, from the first theoretical papers to real world use and implementation.<br/><br/>We will focus on how the original notion led to an "abstract notion of computation" or "abstract computation types", akin to the popular "abstract data types" paradigm. Last, we will present joint work with Prof. Lipton about incorporating the notion of "abstract computation" to logic programming.<br/>

ESC 339