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