Mathematics & Computer Science

Seminars and Colloquia

Computer Science Seminar

Tuesday, February 09, 2016

04:00 pm - 05:30 pm

Computer Science Seminar

Pierre Halmagrand, CEDRIC (Centre d'tude et de Recherche en Informatique et Communications, CNAM) "Automated Deduction and Proof Certification for the B Method Set Theory"

Exley Science Center Tower ESC 638

Tuesday, May 05, 2015

04:15 pm - 05:30 pm

CS Seminar, Brent Yorgey (U. of Penn): 'Derivatives of Data Types, via Regular Expressions'

Abstract: Algebraic data types are central to typed functional programming, sitting at a happy intersection of theory and practice. I will define and give examples of algebraic data types, and then go on to explain what is meant by the derivative of an algebraic data type. In the second part of the talk I will show how to constrain algebraic data types by a given regular expression, including finding derivatives a special case. No particular background is assumed; my goal is to convey not a particular result per se, but rather an appreciation for some of the beautiful overlap between algebra, combinatorics, calculus, and computer science.

ESC 638

Tuesday, April 21, 2015

04:15 pm - 05:30 pm

CS Seminar, Jennifer Paykin (University of Pennsylvania, Wes '12): 'Logic, Categories, and Graphical user Interfaces'

Abstract: The Curry-Howard correspondence equates programming language type systems with mathematical logics. It has allowed researchers to formalize all sorts of interesting language features as type theories, including resource consciousness, control operators, and side effects. But combining such properties in a single language is not always straightforward.In this talk I will propose a unified framework for combining programming features that is based on adjunctions. An adjunction is an ubiquitous relationship between structures in category theory. In the extension of the Curry-Howard correspondence to category theory, it is only natural that adjunctions have an interpretation in type theory as a relationship between two type systems. In the second part of the talk we will explore graphical user interfaces as a concrete use case for our framework. Traditionally GUIs are made up of a collection of widgets (buttons, labels) and some functions, or callbacks, to be executed every time an event (mouse click, key press) occurs. We will explore a programming language that abstracts away first-class callbacks to make them more manageable. In doing so, we will identify which attributes we need such a language to have, and show how these properties fit into our feature framework.

ESC 638

Tuesday, April 07, 2015

04:15 pm - 05:30 pm

Computer Science Seminar, Charles Wallace (Michigan Technological University): 'Preparing students for communication-intensive software development through inquiry, critique and reflection'

Abstract: Among software professionals, the quality of team communication is widely acknowledged to be a key factor in the success or failure of software projects. The inherent mutability and intangibility of software, coupled with the intense rate of change in the software workplace, demand attentiveness and precision in oral and written communication. Students in CISE programs need training from communication specialists and practice in the particular genres common to their future profession. Successful communication in the workplace, however, requires more than technical mastery of common genres presented in isolation; while a software process model can provide guidelines, there is no comprehensive, rote communication workflow. Developers must make strategic communication decisions, and they must be agile ? flexible, proactive, and creative ? in these decisions. We envision an enhanced undergraduate curriculum for CISE programs that promotes agile communication through practice in inquiry, critique and reflection, grounded in authentic software development settings. Communication-intensive activities are woven through this curriculum in a variety of ways. The POGIL framework provides a structured approach to inquiry. Automated feedback on test coverage, programming style and code documentation are provided through CanvasTA, a novel tool integrated into the Canvas LMS, supplementing instructor feedback with continual critique of code and documentation. A program of guided inquiry through real case studies of software communication prepare students for their team software activities, and a series of reflective exercises leads them to focus on their own team communication practices.

ESC 638

Monday, December 01, 2014

04:15 pm - 05:30 pm

CS Seminar, Rusicka Piscak (Yale Univ.)

Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. In addition, I will outline a procedure that synthesizes code snippets from specifications implicitly given in the form of type constraints. As there can be multiple solutions, more than one code snippet can be a good candidate. We use an additional weight function to rank the derived snippets and direct the search for them. In practical evaluation, our technique scales to programs with thousands of visible declarations in scope and succeeds in 0.5 seconds to suggest program expressions of interest. I will conclude with an outlook on possible future research directions and applications of synthesis procedures. Bio: Ruzica Piskac is an assistant professor at Yale, Computer Science Department. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques. Prior to joining Yale, Ruzica was an independent research group leader at the Max Planck Institute for Software Systems (MPI-SWS) in Germany (January 2012-August 2013). She was head of the Synthesis, Analysis and Automated Reasoning Group. Ruzica did her graduate studies at EPFL, Switzerland under the supervision of Viktor Kuncak.

ESC 618

Tuesday, November 18, 2014

04:15 pm - 05:30 pm

CS Seminar, Dan Fasulo (Pattern Genomics): DNA signatures - An idea whose time has finally come

Abstract: DNA signatures are short nucleotide sequences that uniquely identify a class of target organisms such as a specific bacterial species or viral strain. Algorithms to find DNA signatures have been described in bioinformatics literature for over a decade, but only recently has the widespread adoption of next generation DNA sequencing made it feasible for a typical molecular biology laboratory to mine large collections of DNA sequences for signatures. This talk will discuss algorithms for finding DNA signatures and describe how these techniques are poised to revolutionize molecular diagnostics.

ESC 638

Tuesday, November 11, 2014

04:15 pm - 05:30 pm

CS Seminar, John Karro (Univ. of Miami Ohio): The identification and analysis of genomic transposable elements.

Abstract: Transposable Elements, or TEs, are mobile DNA sequences capable of inserting multiple copies of themselves into a genome. Throughout our evolutionary history the human genome has been repeatedly subjected to such insertions, to the point where upward of 45% of our genetic sequence is the remnants of TEs and other repetitive sequences. Identifying these TEs could be easily framed as a basic string-matching problem, were it not for the effect of genetic mutations: while a given TE was initially a copy of its progenitor sequence, over time the DNA sequence changed in an apparently random manner. Thus the identification problem becomes significantly more difficult, and is even further complicated by size of the input which any solution algorithm will be applied. Given the size of the higher-order genomes (e.g. n ≈ 3?109 for human, n ≈ 5x1010 for salamander), any identification algorithm must have runtime and memory usage bounds that scale linearly with input size if the algorithm is to be of practical use. But once TEs have been identified, they provide important information on the very mutation rates that made them so hard to identify ? giving us a window into genomic evolutionary history. This talk will explore how and why we are solving the identification problem. We will describe the algorithm underlying RAIDER, a new tool for the fast de novo identification of transposable elements. Following this we will describe a mathematical model of molecular evolution, based on TE information that will allow for the identification of genes that have undergone a change in their strand-symmetry classification sometime over the last one-hundred million years. Note: This talk will assume an audience with a background in mathematics or the quantitative sciences. No knowledge of biology will be required, though some may be inflicted.

ESC 638

Wednesday, March 26, 2014

01:30 pm - 02:30 pm

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

Abstract: Alpern (1976) is credited with asking the following question: 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? 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.

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.Bio: 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.

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. 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.

ESC 638