From dbp at ccs.neu.edu Thu Jan 12 09:51:04 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 12 Jan 2017 14:51:04 +0000 Subject: [Pl-seminar] 1/27 Seminar: John Vilk, Making the Browser Reasonable for Sane Programmers Message-ID: NUPRL Seminar presents John Vilk University of Massachusetts Amherst Host: Ben Greenman 12:00-1:30PM Friday, January 27th 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Making the Browser Reasonable for Sane Programmers Abstract: Billions of people use browsers to access the web from a variety of devices, but it remains difficult to write and debug the client-side of web applications. The browser exposes unfamiliar, redundant, and incompatible abstractions for a variety of common tasks, preventing developers from adapting existing code written for other platforms. The browser environment is completely event-driven and pervasively concurrent, resulting in complex control flow and race conditions that are difficult to debug. In this talk, I will describe how my research makes it easier to write and debug web applications. Doppio is a JavaScript runtime system that lets developers run unaltered code written in general-purpose languages, such as Java and C/C++, directly inside the browser. Browsix further enhances Doppio with a kernel, processes, and shared operating system resources, letting multiple off-the-shelf programs concurrently interoperate on the same webpage. ReJS is a low-overhead and high-fidelity time-traveling debugger that lets developers instantaneously step forward and backward through a program's execution. ReJS accurately recreates the application's complete behavior, including the GUI and multiple types of race conditions, while producing miniscule and portable application traces. These resources transform the browser into a first-class application platform. Bio: John Vilk is a Ph.D. candidate in the College of Information and Computer Sciences at the University of Massachusetts Amherst. He is a member of the PLASMA lab, and is advised by Emery Berger. John's research aims to improve the browser as an application platform by making it easier to write, debug, and optimize complex web applications. John is a Facebook Fellow (2015), and his work on Doppio: Breaking the Browser Language Barrier is a SIGPLAN Research Highlight (2014) and a PLDI Distinguished Artifact (2014). His research forms the basis of Microsoft ChakraCore's time-traveling debugger and lets millions of people interact with legacy software and games in their browser at the Internet Archive (https://archive.org/). John received his MS from the University of Massachusetts Amherst (2013) and his BS from Worcester Polytechnic Institute (2011). You can learn more about John at his website, https://jvilk.com/. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Jan 20 02:58:33 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 20 Jan 2017 07:58:33 +0000 Subject: [Pl-seminar] Reminder: 1/27 Seminar: John Vilk, Making the Browser Reasonable for Sane Programmers In-Reply-To: References: Message-ID: Reminder: This is next week (and our seminar this semester is on FRIDAY at noon). On Thu, Jan 12, 2017 at 3:51 PM Daniel Patterson wrote: > NUPRL Seminar presents > > John Vilk > University of Massachusetts Amherst > Host: Ben Greenman > > 12:00-1:30PM > Friday, January 27th 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > Making the Browser Reasonable for Sane Programmers > > Abstract: > > Billions of people use browsers to access the web from a variety of > devices, but it remains difficult to write and debug the client-side of web > applications. The browser exposes unfamiliar, redundant, and incompatible > abstractions for a variety of common tasks, preventing developers from > adapting existing code written for other platforms. The browser environment > is completely event-driven and pervasively concurrent, resulting in complex > control flow and race conditions that are difficult to debug. > > In this talk, I will describe how my research makes it easier to write and > debug web applications. Doppio is a JavaScript runtime system that lets > developers run unaltered code written in general-purpose languages, such as > Java and C/C++, directly inside the browser. Browsix further enhances > Doppio with a kernel, processes, and shared operating system resources, > letting multiple off-the-shelf programs concurrently interoperate on the > same webpage. ReJS is a low-overhead and high-fidelity time-traveling > debugger that lets developers instantaneously step forward and backward > through a program's execution. ReJS accurately recreates the application's > complete behavior, including the GUI and multiple types of race conditions, > while producing miniscule and portable application traces. These resources > transform the browser into a first-class application platform. > > > Bio: > > John Vilk is a Ph.D. candidate in the College of Information and Computer > Sciences at the University of Massachusetts Amherst. He is a member of the > PLASMA lab, and is advised by Emery Berger. John's research aims to improve > the browser as an application platform by making it easier to write, debug, > and optimize complex web applications. John is a Facebook Fellow (2015), > and his work on Doppio: Breaking the Browser Language Barrier is a SIGPLAN > Research Highlight (2014) and a PLDI Distinguished Artifact (2014). His > research forms the basis of Microsoft ChakraCore's time-traveling debugger > and lets millions of people interact with legacy software and games in > their browser at the Internet Archive (https://archive.org/). John > received his MS from the University of Massachusetts Amherst (2013) and his > BS from Worcester Polytechnic Institute (2011). > > > You can learn more about John at his website, https://jvilk.com/. > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Jan 20 10:52:25 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 20 Jan 2017 15:52:25 +0000 Subject: [Pl-seminar] 2/3 Seminar: Julia Belyakova, Comparative Study of Generic Programming Features in Object-Oriented Languages Message-ID: NUPRL Seminar presents Julia Belyakova Northeastern University (visiting from Southern Federal University) 12:00-1:30 Friday, February 3, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Comparative Study of Generic Programming Features in Object-Oriented Languages Abstract: Earlier comparative studies of language support for generic programming (GP) have shown that mainstream object-oriented (OO) languages such as C# and Java provide weaker support for GP as compared with functional languages such as Haskell or SML. One reason is that generic mechanisms of C# and Java are based on F-bounded polymorphism, which has certain deficiencies. Some of these deficiencies are eliminated in more recent languages, such as Scala and Kotlin. However, there are peculiarities of object-oriented languages as a whole, which prevent them from being as expressible as Haskell in terms of generic programming. In this talk we will cover the main problems of language support for generic programming in C#/Java as well as other modern object-oriented languages, including Scala and Swift. It turns out that all of these languages follow the same approach to constraining type parameters, which leads to inevitable shortcomings. To overcome them, an alternative approach is suggested in several extensions for OO languages, in particular, JavaGenus. The advantages and drawbacks of both approaches will be discussed in the talk. Bio: Julia Belyakova graduated in 2014 from Southern Federal University (Rostov-on-Don, Russia) as Master of Science in ?Computer Science and Information Technologies?. She is enrolled for PhD program in Southern Federal University and came to Northeastern University as a visiting scientist. She is currently doing research in the area of generic programming for object-oriented languages. You can learn more about Julia at her website, http://staff.mmcs.sfedu.ru/~juliet/index.en.html. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Jan 26 10:52:22 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 26 Jan 2017 15:52:22 +0000 Subject: [Pl-seminar] Reminder: Seminar TOMORROW: John Vilk, Making the Browser Reasonable for Sane Programmers In-Reply-To: References: Message-ID: Reminder: This is tomorrow! On Thu, Jan 12, 2017 at 9:51 AM Daniel Patterson wrote: > NUPRL Seminar presents > > John Vilk > University of Massachusetts Amherst > Host: Ben Greenman > > 12:00-1:30PM > Friday, January 27th 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > Making the Browser Reasonable for Sane Programmers > > Abstract: > > Billions of people use browsers to access the web from a variety of > devices, but it remains difficult to write and debug the client-side of web > applications. The browser exposes unfamiliar, redundant, and incompatible > abstractions for a variety of common tasks, preventing developers from > adapting existing code written for other platforms. The browser environment > is completely event-driven and pervasively concurrent, resulting in complex > control flow and race conditions that are difficult to debug. > > In this talk, I will describe how my research makes it easier to write and > debug web applications. Doppio is a JavaScript runtime system that lets > developers run unaltered code written in general-purpose languages, such as > Java and C/C++, directly inside the browser. Browsix further enhances > Doppio with a kernel, processes, and shared operating system resources, > letting multiple off-the-shelf programs concurrently interoperate on the > same webpage. ReJS is a low-overhead and high-fidelity time-traveling > debugger that lets developers instantaneously step forward and backward > through a program's execution. ReJS accurately recreates the application's > complete behavior, including the GUI and multiple types of race conditions, > while producing miniscule and portable application traces. These resources > transform the browser into a first-class application platform. > > > Bio: > > John Vilk is a Ph.D. candidate in the College of Information and Computer > Sciences at the University of Massachusetts Amherst. He is a member of the > PLASMA lab, and is advised by Emery Berger. John's research aims to improve > the browser as an application platform by making it easier to write, debug, > and optimize complex web applications. John is a Facebook Fellow (2015), > and his work on Doppio: Breaking the Browser Language Barrier is a SIGPLAN > Research Highlight (2014) and a PLDI Distinguished Artifact (2014). His > research forms the basis of Microsoft ChakraCore's time-traveling debugger > and lets millions of people interact with legacy software and games in > their browser at the Internet Archive (https://archive.org/). John > received his MS from the University of Massachusetts Amherst (2013) and his > BS from Worcester Polytechnic Institute (2011). > > > You can learn more about John at his website, https://jvilk.com/. > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Jan 27 18:47:53 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 27 Jan 2017 23:47:53 +0000 Subject: [Pl-seminar] Reminder: 2/3 Seminar (New Location): Julia Belyakova, Comparative Study of Generic Programming Features in Object-Oriented Languages In-Reply-To: References: Message-ID: Reminder: This is NEXT WEEK, and there is a LOCATION CHANGE: The seminar will be held in Cargill Hall, Room 97. Cargill Hall is right next to WVH, and Room 97 was where NEPLS was held in the fall. On Fri, Jan 20, 2017 at 10:52 AM Daniel Patterson wrote: > NUPRL Seminar presents > > Julia Belyakova > Northeastern University (visiting from Southern Federal University) > > 12:00-1:30 > Friday, February 3, 2017 > Room 97 Cargill Hall > > > Comparative Study of Generic Programming Features in Object-Oriented > Languages > > Abstract: > Earlier comparative studies of language support for generic programming > (GP) have shown that mainstream object-oriented (OO) languages such as C# > and Java provide weaker support for GP as compared with functional > languages such as Haskell or SML. > > One reason is that generic mechanisms of C# and Java are based on > F-bounded polymorphism, which has certain deficiencies. Some of these > deficiencies are eliminated in more recent languages, such as Scala and > Kotlin. However, there are peculiarities of object-oriented languages as a > whole, which prevent them from being as expressible as Haskell in terms of > generic programming. > > In this talk we will cover the main problems of language support for > generic programming in C#/Java as well as other modern object-oriented > languages, including Scala and Swift. It turns out that all of these > languages follow the same approach to constraining type parameters, which > leads to inevitable shortcomings. To overcome them, an alternative approach > is suggested in several extensions for OO languages, in particular, > JavaGenus. The advantages and drawbacks of both approaches will be > discussed in the talk. > > Bio: > Julia Belyakova graduated in 2014 from Southern Federal University > (Rostov-on-Don, Russia) as Master of Science in ?Computer Science and > Information Technologies?. She is enrolled for PhD program in Southern > Federal University and came to Northeastern University as a visiting > scientist. She is currently doing research in the area of generic > programming for object-oriented languages. > You can learn more about Julia at her website, > http://staff.mmcs.sfedu.ru/~juliet/index.en.html. > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Feb 2 09:50:18 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 02 Feb 2017 14:50:18 +0000 Subject: [Pl-seminar] Reminder: Seminar TOMORROW: Julia Belyakova, Comparative Study of Generic Programming Features in Object-Oriented Languages In-Reply-To: References: Message-ID: Reminder that this is TOMORROW, and at noon in Cargill Hall, Room 97. Cargill Hall is right next to WVH, and Room 97 was where NEPLS was held in the fall. On Fri, Jan 20, 2017 at 10:52 AM Daniel Patterson wrote: > > NUPRL Seminar presents > > Julia Belyakova > Northeastern University (visiting from Southern Federal University) > > 12:00-1:30 > Friday, February 3, 2017 > Room 97 Cargill Hall > > > Comparative Study of Generic Programming Features in Object-Oriented > Languages > > Abstract: > Earlier comparative studies of language support for generic programming > (GP) have shown that mainstream object-oriented (OO) languages such as C# > and Java provide weaker support for GP as compared with functional > languages such as Haskell or SML. > > One reason is that generic mechanisms of C# and Java are based on > F-bounded polymorphism, which has certain deficiencies. Some of these > deficiencies are eliminated in more recent languages, such as Scala and > Kotlin. However, there are peculiarities of object-oriented languages as a > whole, which prevent them from being as expressible as Haskell in terms of > generic programming. > > In this talk we will cover the main problems of language support for > generic programming in C#/Java as well as other modern object-oriented > languages, including Scala and Swift. It turns out that all of these > languages follow the same approach to constraining type parameters, which > leads to inevitable shortcomings. To overcome them, an alternative approach > is suggested in several extensions for OO languages, in particular, > JavaGenus. The advantages and drawbacks of both approaches will be > discussed in the talk. > > Bio: > Julia Belyakova graduated in 2014 from Southern Federal University > (Rostov-on-Don, Russia) as Master of Science in ?Computer Science and > Information Technologies?. She is enrolled for PhD program in Southern > Federal University and came to Northeastern University as a visiting > scientist. She is currently doing research in the area of generic > programming for object-oriented languages. > You can learn more about Julia at her website, > http://staff.mmcs.sfedu.ru/~juliet/index.en.html. > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Feb 10 12:53:23 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 10 Feb 2017 17:53:23 +0000 Subject: [Pl-seminar] 2/24 Seminar: Ben Sherman, Overlapping pattern matching for programming with continuous functions Message-ID: NUPRL Seminar presents Ben Sherman MIT Host: Gabriel Scherer 12:00pm Friday, February 24, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Overlapping pattern matching for programming with continuous functions Abstract: Topology, when viewed from an unusual perspective (formal topology), describes how to compute with certain objects that are beyond the reach of induction, such as real numbers, probability distributions, streams, and function spaces. Accordingly, one gets a programming language whose types are spaces and whose functions are continuous maps. Does this language have pattern matching? In functional programming, pattern matching allows definition of a function by partitioning the input and defining the result in each case. We generalize to programming with spaces, where patterns need not represent decidable predicates and also may overlap, potentially allowing nondeterministic behavior in overlapping regions. These overlapping pattern matches are useful for writing a wide array of computer programs on spaces, such as programs that make approximate computations or decisions based on continuous values or that manipulate "partial" datatypes. This talk will introduce topology from a computational perspective, and explore some programs that can be built with this framework using overlapping pattern matching. Bio: Ben Sherman is a second-year PhD student at MIT, advised by Adam Chlipala and Michael Carbin. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Mon Feb 20 16:46:06 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Mon, 20 Feb 2017 21:46:06 +0000 Subject: [Pl-seminar] Reminder: 2/24 Seminar: Ben Sherman, Overlapping pattern matching for programming with continuous functions In-Reply-To: References: Message-ID: Reminder: This is Friday! On Fri, Feb 10, 2017 at 12:53 PM Daniel Patterson wrote: > NUPRL Seminar presents > > Ben Sherman > MIT > Host: Gabriel Scherer > > 12:00pm > Friday, February 24, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Overlapping pattern matching for programming with continuous functions > > Abstract: > > Topology, when viewed from an unusual perspective (formal topology), > describes how to compute with certain objects that are beyond the reach of > induction, such as real numbers, probability distributions, streams, and > function spaces. Accordingly, one gets a programming language whose types > are spaces and whose functions are continuous maps. > > Does this language have pattern matching? In functional programming, > pattern matching allows definition of a function by partitioning the input > and defining the result in each case. We generalize to programming with > spaces, where patterns need not represent decidable predicates and also may > overlap, potentially allowing nondeterministic behavior in overlapping > regions. These overlapping pattern matches are useful for writing a wide > array of computer programs on spaces, such as programs that make > approximate computations or decisions based on continuous values or that > manipulate "partial" datatypes. > > This talk will introduce topology from a computational perspective, and > explore some programs that can be built with this framework using > overlapping pattern matching. > > Bio: > > Ben Sherman is a second-year PhD student at MIT, advised by Adam Chlipala > and Michael Carbin. > > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Feb 23 10:35:48 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 23 Feb 2017 15:35:48 +0000 Subject: [Pl-seminar] Reminder: 2/24 Seminar: Ben Sherman, Overlapping pattern matching for programming with continuous functions In-Reply-To: References: Message-ID: Reminder - this is tomorrow! On Mon, Feb 20, 2017 at 4:45 PM Daniel Patterson wrote: > Reminder: This is Friday! > > On Fri, Feb 10, 2017 at 12:53 PM Daniel Patterson wrote: > > NUPRL Seminar presents > > Ben Sherman > MIT > Host: Gabriel Scherer > > 12:00pm > Friday, February 24, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Overlapping pattern matching for programming with continuous functions > > Abstract: > > Topology, when viewed from an unusual perspective (formal topology), > describes how to compute with certain objects that are beyond the reach of > induction, such as real numbers, probability distributions, streams, and > function spaces. Accordingly, one gets a programming language whose types > are spaces and whose functions are continuous maps. > > Does this language have pattern matching? In functional programming, > pattern matching allows definition of a function by partitioning the input > and defining the result in each case. We generalize to programming with > spaces, where patterns need not represent decidable predicates and also may > overlap, potentially allowing nondeterministic behavior in overlapping > regions. These overlapping pattern matches are useful for writing a wide > array of computer programs on spaces, such as programs that make > approximate computations or decisions based on continuous values or that > manipulate "partial" datatypes. > > This talk will introduce topology from a computational perspective, and > explore some programs that can be built with this framework using > overlapping pattern matching. > > Bio: > > Ben Sherman is a second-year PhD student at MIT, advised by Adam Chlipala > and Michael Carbin. > > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Feb 24 14:56:44 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 24 Feb 2017 19:56:44 +0000 Subject: [Pl-seminar] 3/10 Seminar: Jimmy Hartzell, Templates and Types in C++ Message-ID: NUPRL Seminar presents Jimmy Hartzell Tower Research Host: Ben Greenman 12:00-1:30 Friday, Mar 10, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Templates and Types in C++ Abstract: Like many modern programming languages, C++ supports both generic programming (templates) and object-oriented programming (inheritance and virtual functions). Unlike many modern programming languages, the generic programming mechanism does not fully leverage or interact with the type system. It amounts to compile-time duck typing: C++ function templates, like functions from a non-statically typed programming language, have their full interface implicit in their implementations -- making it hard to discern what that interface actually is. The concept of Concepts (compile-time typeclasses) was slated for introduction into C++ in the C++11 version of the standard, then C++14, then C++17, now C++20... What can we do to work around their absence? Relatedly, how do we bridge the gap between static and dynamic polymorphism? C++ provides both, and sometimes we want to mix and mash them. Template tricks can also be done to accomplish this as well. Bio Jimmy Hartzell is a software developer and C++ instructor at Tower Research. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Mar 3 10:46:28 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 03 Mar 2017 15:46:28 +0000 Subject: [Pl-seminar] 3/10 Seminar: Jimmy Hartzell, Templates and Types in C++ In-Reply-To: References: Message-ID: Reminder - this is next week! On Fri, Feb 24, 2017 at 2:56 PM Daniel Patterson wrote: > NUPRL Seminar presents > > Jimmy Hartzell > Tower Research > Host: Ben Greenman > > 12:00-1:30 > Friday, Mar 10, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Templates and Types in C++ > > Abstract: > > Like many modern programming languages, C++ supports both generic > programming (templates) and object-oriented programming (inheritance and > virtual functions). Unlike many modern programming languages, the generic > programming mechanism does not fully leverage or interact with the type > system. It amounts to compile-time duck typing: C++ function templates, > like functions from a non-statically typed programming language, have their > full interface implicit in their implementations -- making it hard to > discern what that interface actually is. The concept of Concepts > (compile-time typeclasses) was slated for introduction into C++ in the > C++11 version of the standard, then C++14, then C++17, now C++20... What > can we do to work around their absence? > > Relatedly, how do we bridge the gap between static and dynamic > polymorphism? C++ provides both, and sometimes we want to mix and mash > them. Template tricks can also be done to accomplish this as well. > > Bio > > Jimmy Hartzell is a software developer and C++ instructor at Tower > Research. > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Mar 9 09:31:00 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 09 Mar 2017 14:31:00 +0000 Subject: [Pl-seminar] 3/10 Seminar: Jimmy Hartzell, Templates and Types in C++ In-Reply-To: References: Message-ID: Reminder - this is tomorrow! On Fri, Feb 24, 2017 at 2:56 PM Daniel Patterson wrote: > NUPRL Seminar presents > > Jimmy Hartzell > Tower Research > Host: Ben Greenman > > 12:00-1:30 > Friday, Mar 10, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Templates and Types in C++ > > Abstract: > > Like many modern programming languages, C++ supports both generic > programming (templates) and object-oriented programming (inheritance and > virtual functions). Unlike many modern programming languages, the generic > programming mechanism does not fully leverage or interact with the type > system. It amounts to compile-time duck typing: C++ function templates, > like functions from a non-statically typed programming language, have their > full interface implicit in their implementations -- making it hard to > discern what that interface actually is. The concept of Concepts > (compile-time typeclasses) was slated for introduction into C++ in the > C++11 version of the standard, then C++14, then C++17, now C++20... What > can we do to work around their absence? > > Relatedly, how do we bridge the gap between static and dynamic > polymorphism? C++ provides both, and sometimes we want to mix and mash > them. Template tricks can also be done to accomplish this as well. > > Bio > > Jimmy Hartzell is a software developer and C++ instructor at Tower > Research. > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Sun Mar 12 12:14:37 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Sun, 12 Mar 2017 16:14:37 +0000 Subject: [Pl-seminar] 3/24 Seminar: Swarat Chaudhuri, Learning to Program and Debug, Automatically Message-ID: NUPRL Seminar presents Swarat Chaudhuri Rice University Host: Amal Ahmed 12:00-1:30PM Friday, March 24, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Learning to Program and Debug, Automatically Abstract: Automating programming and debugging are long-standing goals in computer science. In spite of significant progress in formal methods over the years, we remain very far from achieving these goals. For example, a freshman CS major will typically program circles around today's best program synthesizers. Debugging and verification tools rely on formal specifications, which are hard to provide in many important applications. Two critical components of the gap between human and machine programmers are that humans learn from experience, i.e., data, and can easily generalize from incomplete problem definitions. In this talk, I will present a general framework for formal methods, based on Bayesian statistical learning, that aims to eliminate these differences. In our framework, descriptions of programming tasks are seen to be "clues" towards a hidden (probabilistic) specification that fully defines the task. Large corpora of real-world programs are used to construct a statistical model that correlates specifications with the form and function of their implementations. The framework can be implemented in a variety of ways, but in particular, through a neural architecture called Bayesian variational encoder-decoders. Inferences made using the framework can be used to guide traditional algorithms for program synthesis and bug-finding. I will show that this data-driven approach can lead to giant leaps in the scope and performance of automated program synthesis and debugging algorithms. Specifically, I will give a demo of Bayou, a system for Bayesian inductive synthesis of Java programs that goes significantly beyond the state of the art in program synthesis. I will also describe Salento, a debugging system based on our framework that can find subtle violations of API contracts without any kind of specification. Bio: Swarat Chaudhuri is an Associate Professor of Computer Science at Rice University. His research lies at the interface of programming systems and artificial intelligence. Much of his recent work is on program synthesis, the problem of automatically generating computer programs from high-level specifications. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Mon Mar 20 09:28:08 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Mon, 20 Mar 2017 13:28:08 +0000 Subject: [Pl-seminar] Reminder: 3/24 Seminar: Swarat Chaudhuri, Learning to Program and Debug, Automatically In-Reply-To: References: Message-ID: Reminder: This is Friday! On Sun, Mar 12, 2017 at 12:14 PM Daniel Patterson wrote: > NUPRL Seminar presents > > Swarat Chaudhuri > Rice University > Host: Amal Ahmed > > 12:00-1:30PM > Friday, March 24, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Learning to Program and Debug, Automatically > > Abstract: > > Automating programming and debugging are long-standing goals in computer > science. In spite of significant progress in formal methods over the years, > we remain very far from achieving these goals. For example, a freshman CS > major will typically program circles around today's best program > synthesizers. Debugging and verification tools rely on formal > specifications, which are hard to provide in many important applications. > > Two critical components of the gap between human and machine programmers > are that humans learn from experience, i.e., data, and can easily > generalize from incomplete problem definitions. In this talk, I will > present a general framework for formal methods, based on Bayesian > statistical learning, that aims to eliminate these differences. In our > framework, descriptions of programming tasks are seen to be "clues" towards > a hidden (probabilistic) specification that fully defines the task. Large > corpora of real-world programs are used to construct a statistical model > that correlates specifications with the form and function of their > implementations. The framework can be implemented in a variety of ways, but > in particular, through a neural architecture called Bayesian variational > encoder-decoders. Inferences made using the framework can be used to guide > traditional algorithms for program synthesis and bug-finding. > > I will show that this data-driven approach can lead to giant leaps in the > scope and performance of automated program synthesis and debugging > algorithms. Specifically, I will give a demo of Bayou, a system for > Bayesian inductive synthesis of Java programs that goes significantly > beyond the state of the art in program synthesis. I will also describe > Salento, a debugging system based on our framework that can find subtle > violations of API contracts without any kind of specification. > > Bio: > > Swarat Chaudhuri is an Associate Professor of Computer Science at Rice > University. His research lies at the interface of programming systems and > artificial intelligence. Much of his recent work is on program synthesis, > the problem of automatically generating computer programs from high-level > specifications. > > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Mon Mar 20 09:39:11 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Mon, 20 Mar 2017 13:39:11 +0000 Subject: [Pl-seminar] 3/31 Seminar: Mooly Sagiv, Simple Invariants for proving the safety of distributed protocols and networks Message-ID: NUPRL Seminar presents Mooly Sagiv Tel Aviv University Host: Jan Vitek and Frank Tip 12:00-1:30PM Friday, March 31st, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Simple Invariants for proving the safety of distributed protocols and networks Abstract: Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants --- an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver. This is a joint work with Ken McMillan (MSR), Oded Padon (TAU), Aurojit Panda(Berkeley) , and Sharon Shoham(TAU) and was integrated into the IVY system: http://www.cs.tau.ac.il/~odedp/ivy/. The work is inspired by Shachar Itzhaky's thesis available from http://people.csail.mit.edu/shachari/ Bio: Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya Inc acquired by Infosys. He received best-paper awards at PLDI'11 and PLDI'12 for his work on composing concurrent data structures and a ACM SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is an ACM fellow and a recipient of Microsoft Research Outstanding Collaborator Award 2016. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Mar 23 10:09:55 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 23 Mar 2017 14:09:55 +0000 Subject: [Pl-seminar] 3/24 Seminar: Swarat Chaudhuri, Learning to Program and Debug, Automatically In-Reply-To: References: Message-ID: Reminder - this is tomorrow! On Sun, Mar 12, 2017 at 12:14 PM Daniel Patterson wrote: > NUPRL Seminar presents > > Swarat Chaudhuri > Rice University > Host: Amal Ahmed > > 12:00-1:30PM > Friday, March 24, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Learning to Program and Debug, Automatically > > Abstract: > > Automating programming and debugging are long-standing goals in computer > science. In spite of significant progress in formal methods over the years, > we remain very far from achieving these goals. For example, a freshman CS > major will typically program circles around today's best program > synthesizers. Debugging and verification tools rely on formal > specifications, which are hard to provide in many important applications. > > Two critical components of the gap between human and machine programmers > are that humans learn from experience, i.e., data, and can easily > generalize from incomplete problem definitions. In this talk, I will > present a general framework for formal methods, based on Bayesian > statistical learning, that aims to eliminate these differences. In our > framework, descriptions of programming tasks are seen to be "clues" towards > a hidden (probabilistic) specification that fully defines the task. Large > corpora of real-world programs are used to construct a statistical model > that correlates specifications with the form and function of their > implementations. The framework can be implemented in a variety of ways, but > in particular, through a neural architecture called Bayesian variational > encoder-decoders. Inferences made using the framework can be used to guide > traditional algorithms for program synthesis and bug-finding. > > I will show that this data-driven approach can lead to giant leaps in the > scope and performance of automated program synthesis and debugging > algorithms. Specifically, I will give a demo of Bayou, a system for > Bayesian inductive synthesis of Java programs that goes significantly > beyond the state of the art in program synthesis. I will also describe > Salento, a debugging system based on our framework that can find subtle > violations of API contracts without any kind of specification. > > Bio: > > Swarat Chaudhuri is an Associate Professor of Computer Science at Rice > University. His research lies at the interface of programming systems and > artificial intelligence. Much of his recent work is on program synthesis, > the problem of automatically generating computer programs from high-level > specifications. > > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Sat Mar 25 10:06:57 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Sat, 25 Mar 2017 14:06:57 +0000 Subject: [Pl-seminar] Reminder: 3/31 Seminar: Mooly Sagiv, Simple Invariants for proving the safety of distributed protocols and networks In-Reply-To: References: Message-ID: Reminder - this is next week. On Mon, Mar 20, 2017 at 9:39 AM Daniel Patterson wrote: > NUPRL Seminar presents > > Mooly Sagiv > Tel Aviv University > Host: Jan Vitek and Frank Tip > > 12:00-1:30PM > Friday, March 31st, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Simple Invariants for proving the safety of distributed protocols and > networks > > Abstract: > > Safety of a distributed protocol means that the protocol never reaches a > bad state, e.g., a state where two nodes become leaders in a > leader-election protocol. Proving safety is obviously undecidable since > such protocols are run by an unbounded number of nodes, and their safety > needs to be established for any number of nodes. I will describe a > deductive approach for proving safety, based on the concept of universally > quantified inductive invariants --- an adaptation of the mathematical > concept of induction to the domain of programs. In the deductive approach, > the programmer specifies a candidate inductive invariant and the system > automatically checks if it is inductive. By restricting the invariants to > be universally quantified, this approach can be effectively implemented > with a SAT solver. > > This is a joint work with Ken McMillan (MSR), Oded Padon (TAU), Aurojit > Panda(Berkeley) , and Sharon Shoham(TAU) and was integrated into the IVY > system: http://www.cs.tau.ac.il/~odedp/ivy/. The work is inspired by > Shachar Itzhaky's thesis available from > http://people.csail.mit.edu/shachari/ > > Bio: > > Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv > University. He is a leading researcher in the area of large scale > (inter-procedural) program analysis, and one of the key contributors to > shape analysis. His fields of interests include programming languages, > compilers, abstract interpretation, profiling, pointer analysis, shape > analysis, inter-procedural dataflow analysis, program slicing, and > language-based programming environments. Sagiv is a recipient of a 2013 > senior ERC research grant for Verifying and Synthesizing Software > Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya > Inc acquired by Infosys. He received best-paper awards at PLDI'11 and > PLDI'12 for his work on composing concurrent data structures and a ACM > SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is > an ACM fellow and a recipient of Microsoft Research Outstanding > Collaborator Award 2016. > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Mar 30 12:48:03 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 30 Mar 2017 12:48:03 -0400 Subject: [Pl-seminar] 3/31 Seminar: Mooly Sagiv, Simple Invariants for proving the safety of distributed protocols and networks In-Reply-To: References: Message-ID: Reminder - this is tomorrow! On Mon, Mar 20, 2017 at 9:39 AM, Daniel Patterson wrote: > NUPRL Seminar presents > > Mooly Sagiv > Tel Aviv University > Host: Jan Vitek and Frank Tip > > 12:00-1:30PM > Friday, March 31st, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Simple Invariants for proving the safety of distributed protocols and > networks > > Abstract: > > Safety of a distributed protocol means that the protocol never reaches a > bad state, e.g., a state where two nodes become leaders in a > leader-election protocol. Proving safety is obviously undecidable since > such protocols are run by an unbounded number of nodes, and their safety > needs to be established for any number of nodes. I will describe a > deductive approach for proving safety, based on the concept of universally > quantified inductive invariants --- an adaptation of the mathematical > concept of induction to the domain of programs. In the deductive approach, > the programmer specifies a candidate inductive invariant and the system > automatically checks if it is inductive. By restricting the invariants to > be universally quantified, this approach can be effectively implemented > with a SAT solver. > > This is a joint work with Ken McMillan (MSR), Oded Padon (TAU), Aurojit > Panda(Berkeley) , and Sharon Shoham(TAU) and was integrated into the IVY > system: http://www.cs.tau.ac.il/~odedp/ivy/. The work is inspired by > Shachar Itzhaky's thesis available from http://people.csail.mit.edu/ > shachari/ > > Bio: > > Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv > University. He is a leading researcher in the area of large scale > (inter-procedural) program analysis, and one of the key contributors to > shape analysis. His fields of interests include programming languages, > compilers, abstract interpretation, profiling, pointer analysis, shape > analysis, inter-procedural dataflow analysis, program slicing, and > language-based programming environments. Sagiv is a recipient of a 2013 > senior ERC research grant for Verifying and Synthesizing Software > Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya > Inc acquired by Infosys. He received best-paper awards at PLDI'11 and > PLDI'12 for his work on composing concurrent data structures and a ACM > SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is > an ACM fellow and a recipient of Microsoft Research Outstanding > Collaborator Award 2016. > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Mar 31 19:12:19 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 31 Mar 2017 19:12:19 -0400 Subject: [Pl-seminar] 4/14 Seminar: Magnus Madsen, From Datalog to Flix: A Declarative Language for Fixed Points on Lattices Message-ID: NOTE: Due to a scheduling issue, this seminar will be held starting at *1:30pm*, rather than our normal time. NUPRL Seminar presents Magnus Madsen University of Waterloo Host: Frank Tip 1:30-3:00PM Friday, April 14th 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) >From Datalog to Flix: A Declarative Language for Fixed Points on Lattices Abstract: We present FLIX, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-na?ve evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of FLIX clearly exposes the similarity between these two algorithms. This work has previously been presented at PLDI 2016. The talk will cover some of that material as well as recent developments. Bio: The speaker is a post doctoral fellow at the University of Waterloo. -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Fri Apr 7 16:19:37 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 7 Apr 2017 16:19:37 -0400 Subject: [Pl-seminar] Reminder: 4/14 Seminar: Magnus Madsen, From Datalog to Flix: A Declarative Language for Fixed Points on Lattices Message-ID: Reminder, this is next week at *1:30PM.* On Fri, Mar 31, 2017 at 7:12 PM, Daniel Patterson wrote: > NOTE: Due to a scheduling issue, this seminar will be held starting at > *1:30pm*, rather than our normal time. > > NUPRL Seminar presents > > Magnus Madsen > University of Waterloo > Host: Frank Tip > > 1:30-3:00PM > Friday, April 14th 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > From Datalog to Flix: A Declarative Language for Fixed Points on Lattices > > Abstract: > We present FLIX, a declarative programming language for > specifying and solving least fixed point problems, particularly > static program analyses. FLIX is inspired by Datalog and > extends it with lattices and monotone functions. Using FLIX, > implementors of static analyses can express a broader range > of analyses than is currently possible in pure Datalog, while > retaining its familiar rule-based syntax. > We define a model-theoretic semantics of FLIX as a natural > extension of the Datalog semantics. This semantics captures > the declarative meaning of FLIX programs without imposing > any specific evaluation strategy. An efficient strategy is > semi-na?ve evaluation which we adapt for FLIX. We have > implemented a compiler and runtime for FLIX, and used it > to express several well-known static analyses, including the > IFDS and IDE algorithms. The declarative nature of FLIX > clearly exposes the similarity between these two algorithms. > > This work has previously been presented at PLDI 2016. > The talk will cover some of that material as well as recent developments. > > > Bio: > The speaker is a post doctoral fellow at the University of Waterloo. > > -------------- next part -------------- HTML attachment scrubbed and removed From dbp at ccs.neu.edu Thu Apr 13 09:54:15 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 13 Apr 2017 09:54:15 -0400 Subject: [Pl-seminar] Reminder: Seminar TOMORROW: Magnus Madsen, From Datalog to Flix: A Declarative Language for Fixed Points on Lattices In-Reply-To: References: Message-ID: Reminder -- this is tomorrow, and it is at 1:30PM, which is NOT our normal time. Daniel Patterson writes: > NOTE: Due to a scheduling issue, this seminar will be held starting at > *1:30pm*, rather than our normal time. > > NUPRL Seminar presents > > Magnus Madsen > University of Waterloo > Host: Frank Tip > > 1:30-3:00PM > Friday, April 14th 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > From Datalog to Flix: A Declarative Language for Fixed Points on Lattices > > Abstract: > We present FLIX, a declarative programming language for > specifying and solving least fixed point problems, particularly > static program analyses. FLIX is inspired by Datalog and > extends it with lattices and monotone functions. Using FLIX, > implementors of static analyses can express a broader range > of analyses than is currently possible in pure Datalog, while > retaining its familiar rule-based syntax. > We define a model-theoretic semantics of FLIX as a natural > extension of the Datalog semantics. This semantics captures > the declarative meaning of FLIX programs without imposing > any specific evaluation strategy. An efficient strategy is > semi-na?ve evaluation which we adapt for FLIX. We have > implemented a compiler and runtime for FLIX, and used it > to express several well-known static analyses, including the > IFDS and IDE algorithms. The declarative nature of FLIX > clearly exposes the similarity between these two algorithms. > > This work has previously been presented at PLDI 2016. > The talk will cover some of that material as well as recent developments. > > > Bio: > The speaker is a post doctoral fellow at the University of Waterloo. From dbp at ccs.neu.edu Mon Apr 24 15:47:26 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Mon, 24 Apr 2017 15:47:26 -0400 Subject: [Pl-seminar] 5/5 Seminar: Multi-language programming system: a linear experiment Message-ID: NUPRL Seminar presents 12:00-1:30PM May 5, 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Multi-language programming system: a linear experiment Abstract: Programming language research keeps inventing more powerful dynamic and static features for programming language. Ideally, thorough language design should be able to propose a single, unified, powerful yet simple view of them as orthogonal aspects of a single programming language that would remain usable by everyone. In practice, it always takes much more time and effort to find the simple/orthogonal presentation than to come up with the desirable features, and we become emotionally attached to programming language monoliths (C++, Scala, GHC Haskell, OCaml, Common Lisp...) that suffer from feature creep. An alternative is to design programming systems as multi-language environment instead. This point of view makes it easier to detect flaws in a proposed programming system design: there is no clear objective definition of what "orthogonal features" really mean, but we have clear ideas of how multi-language systems should work. The Racket Manifesto says: "Each language and component must be able to protect its specific invariants". In this work we give a formal specification, in terms of full abstraction, for what it means for a new language added to the system to not introduce "abstraction leaks" in the other languages, and discuss scenarios where this translates in (informal) usability properties: having a nice teachable language subset, or gracefully introducing an advanced language for experts. We present a multi-language design that exhibits this formal property by adding a language L with linear types and linear state to a typical ML-style programming language U. L allows to write programs with resource usage guarantees (space consumption, typestate-style safety guarantees) that were not possible in U, without introducing abstraction leaks. We will demonstrate several useful examples, some of them that crucially rely on the fine-grained use of language boundaries, at a subterm level rather than whole-module level. NOTE: This announcement does not include the author, as this work is currently under submission. From matthias at ccs.neu.edu Mon Apr 24 17:15:20 2017 From: matthias at ccs.neu.edu (Matthias Felleisen) Date: Mon, 24 Apr 2017 17:15:20 -0400 Subject: [Pl-seminar] 5/5 Seminar: Multi-language programming system: a linear experiment In-Reply-To: References: Message-ID: You mean these authors: http://www.ccs.neu.edu/home/amal/ahmed-cv.pdf Really? :-) > On Apr 24, 2017, at 3:47 PM, Daniel Patterson wrote: > > > NUPRL Seminar presents > > 12:00-1:30PM > May 5, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Multi-language programming system: a linear experiment > > Abstract: > > Programming language research keeps inventing more powerful dynamic and > static features for programming language. Ideally, thorough language > design should be able to propose a single, unified, powerful yet simple > view of them as orthogonal aspects of a single programming language that > would remain usable by everyone. In practice, it always takes much more > time and effort to find the simple/orthogonal presentation than to come > up with the desirable features, and we become emotionally attached to > programming language monoliths (C++, Scala, GHC Haskell, OCaml, Common > Lisp...) that suffer from feature creep. An alternative is to design > programming systems as multi-language environment instead. This point of > view makes it easier to detect flaws in a proposed programming system > design: there is no clear objective definition of what "orthogonal > features" really mean, but we have clear ideas of how multi-language > systems should work. The Racket Manifesto says: "Each language and > component must be able to protect its specific invariants". > > In this work we give a formal specification, in terms of full > abstraction, for what it means for a new language added to the system to > not introduce "abstraction leaks" in the other languages, and discuss > scenarios where this translates in (informal) usability properties: > having a nice teachable language subset, or gracefully introducing an > advanced language for experts. We present a multi-language design that > exhibits this formal property by adding a language L with linear types > and linear state to a typical ML-style programming language U. L allows > to write programs with resource usage guarantees (space consumption, > typestate-style safety guarantees) that were not possible in U, without > introducing abstraction leaks. We will demonstrate several useful > examples, some of them that crucially rely on the fine-grained use of > language boundaries, at a subterm level rather than whole-module level. > > NOTE: This announcement does not include the author, as this work is > currently under submission. > > _______________________________________________ > pl-seminar mailing list > pl-seminar at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/pl-seminar From dbp at ccs.neu.edu Fri Apr 28 11:44:29 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 28 Apr 2017 11:44:29 -0400 Subject: [Pl-seminar] Reminder: 5/5 Seminar: Multi-language programming system: a linear experiment In-Reply-To: References: Message-ID: Reminder -- this is next Friday. Daniel Patterson writes: > NUPRL Seminar presents > > 12:00-1:30PM > May 5, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Multi-language programming system: a linear experiment > > Abstract: > > Programming language research keeps inventing more powerful dynamic and > static features for programming language. Ideally, thorough language > design should be able to propose a single, unified, powerful yet simple > view of them as orthogonal aspects of a single programming language that > would remain usable by everyone. In practice, it always takes much more > time and effort to find the simple/orthogonal presentation than to come > up with the desirable features, and we become emotionally attached to > programming language monoliths (C++, Scala, GHC Haskell, OCaml, Common > Lisp...) that suffer from feature creep. An alternative is to design > programming systems as multi-language environment instead. This point of > view makes it easier to detect flaws in a proposed programming system > design: there is no clear objective definition of what "orthogonal > features" really mean, but we have clear ideas of how multi-language > systems should work. The Racket Manifesto says: "Each language and > component must be able to protect its specific invariants". > > In this work we give a formal specification, in terms of full > abstraction, for what it means for a new language added to the system to > not introduce "abstraction leaks" in the other languages, and discuss > scenarios where this translates in (informal) usability properties: > having a nice teachable language subset, or gracefully introducing an > advanced language for experts. We present a multi-language design that > exhibits this formal property by adding a language L with linear types > and linear state to a typical ML-style programming language U. L allows > to write programs with resource usage guarantees (space consumption, > typestate-style safety guarantees) that were not possible in U, without > introducing abstraction leaks. We will demonstrate several useful > examples, some of them that crucially rely on the fine-grained use of > language boundaries, at a subterm level rather than whole-module level. > > NOTE: This announcement does not include the author, as this work is > currently under submission. > > _______________________________________________ > pl-seminar mailing list > pl-seminar at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/pl-seminar From dbp at ccs.neu.edu Thu May 4 10:47:51 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 04 May 2017 10:47:51 -0400 Subject: [Pl-seminar] Reminder: Seminar TOMORROW: Multi-language programming system: a linear experiment In-Reply-To: References: Message-ID: Reminder that this is tomorrow! Daniel Patterson writes: > NUPRL Seminar presents > > 12:00-1:30PM > May 5, 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Multi-language programming system: a linear experiment > > Abstract: > > Programming language research keeps inventing more powerful dynamic and > static features for programming language. Ideally, thorough language > design should be able to propose a single, unified, powerful yet simple > view of them as orthogonal aspects of a single programming language that > would remain usable by everyone. In practice, it always takes much more > time and effort to find the simple/orthogonal presentation than to come > up with the desirable features, and we become emotionally attached to > programming language monoliths (C++, Scala, GHC Haskell, OCaml, Common > Lisp...) that suffer from feature creep. An alternative is to design > programming systems as multi-language environment instead. This point of > view makes it easier to detect flaws in a proposed programming system > design: there is no clear objective definition of what "orthogonal > features" really mean, but we have clear ideas of how multi-language > systems should work. The Racket Manifesto says: "Each language and > component must be able to protect its specific invariants". > > In this work we give a formal specification, in terms of full > abstraction, for what it means for a new language added to the system to > not introduce "abstraction leaks" in the other languages, and discuss > scenarios where this translates in (informal) usability properties: > having a nice teachable language subset, or gracefully introducing an > advanced language for experts. We present a multi-language design that > exhibits this formal property by adding a language L with linear types > and linear state to a typical ML-style programming language U. L allows > to write programs with resource usage guarantees (space consumption, > typestate-style safety guarantees) that were not possible in U, without > introducing abstraction leaks. We will demonstrate several useful > examples, some of them that crucially rely on the fine-grained use of > language boundaries, at a subterm level rather than whole-module level. > > NOTE: This announcement does not include the author, as this work is > currently under submission. > > _______________________________________________ > pl-seminar mailing list > pl-seminar at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/pl-seminar From dbp at ccs.neu.edu Thu May 18 10:15:26 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Thu, 18 May 2017 10:15:26 -0400 Subject: [Pl-seminar] 6/1 Seminar: Cesare Tinelli, CoCoSpec: A Mode-aware Contract Language for Reactive Systems Message-ID: NUPRL Seminar presents Cesare Tinelli University of Iowa Host: Thomas Wahl 11AM-12:30PM (NOTE: THIS IS EARLIER THAN OUR NORMAL TIME!) Thursday, June 1st, 2017 (NOTE: THIS IS NOT OUR STANDARD DAY OF WEEK!) Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) CoCoSpec: A Mode-aware Contract Language for Reactive Systems Abstract: Contract-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Contracts are an effective way to establish boundaries between components and can be used efficiently to verify global properties by using compositional reasoning techniques. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Requirements in the specification of a component are often case-based, with each case describing what the component should do depending on a specific situation (or mode) the component is in. This talk introduces CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems. CoCoSpec is built as an extension of the Lustre language and lets users specify mode behavior directly, instead of encoding it as conditional guarantees, thus preventing a loss of mode-specific information. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness of the compositional analysis techniques found in assume-guarantee frameworks and improve scalability. Such tools can also produce much better feedback during the verification process, as well as valuable qualitative information on the contract itself. I will presents the CoCoSpec language and illustrate the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based model checker developed at the University of Iowa that provides full support for CoCoSpec. Bio: Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in 1999 and is currently a professor in Computer Science at the University of Iowa. His research interests include automated reasoning and formal methods. He has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, General Electric, Rockwell Collins, and United Technologies) and has appeared in more than 70 refereed publications. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has led the development of the award winning Darwin theorem prover and the Kind model checker. He co-leads the development of CVC4,a widely used and award winning SMT solver, and StarExec, a cross community web-based service for the comparative evaluation of logic solvers. From dbp at ccs.neu.edu Fri May 26 12:15:34 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Fri, 26 May 2017 12:15:34 -0400 Subject: [Pl-seminar] Reminder: 6/1 Seminar: Cesare Tinelli, CoCoSpec: A Mode-aware Contract Language for Reactive Systems In-Reply-To: References: Message-ID: Reminder: This is next week, but it is on Thursday (not our normal day), and at 11AM (not our normal time). Daniel Patterson writes: > NUPRL Seminar presents > > Cesare Tinelli > University of Iowa > Host: Thomas Wahl > > 11AM-12:30PM (NOTE: THIS IS EARLIER THAN OUR NORMAL TIME!) > Thursday, June 1st, 2017 (NOTE: THIS IS NOT OUR STANDARD DAY OF WEEK!) > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > CoCoSpec: A Mode-aware Contract Language for Reactive Systems > > Abstract: > > Contract-based software development is a leading methodology for the > construction of safety- and mission-critical embedded systems. Contracts > are an effective way to establish boundaries between components and can > be used efficiently to verify global properties by using compositional > reasoning techniques. A contract specifies the assumptions a component > makes on its context and the guarantees it provides. Requirements in the > specification of a component are often case-based, with each case > describing what the component should do depending on a specific > situation (or mode) the component is in. > > This talk introduces CoCoSpec, a mode-aware assume-guarantee-based > contract language for embedded systems. CoCoSpec is built as an > extension of the Lustre language and lets users specify mode behavior > directly, instead of encoding it as conditional guarantees, thus > preventing a loss of mode-specific information. Mode-aware model > checkers supporting CoCoSpec can increase the effectiveness of the > compositional analysis techniques found in assume-guarantee frameworks > and improve scalability. Such tools can also produce much better > feedback during the verification process, as well as valuable > qualitative information on the contract itself. I will presents the > CoCoSpec language and illustrate the benefits of mode-aware > model-checking on a case study involving a flight-critical avionics > system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based > model checker developed at the University of Iowa that provides full > support for CoCoSpec. > > Bio: > > Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in > 1999 and is currently a professor in Computer Science at the University > of Iowa. His research interests include automated reasoning and formal > methods. He has done seminal work in automated reasoning, in particular > in Satisfiability Modulo Theories (SMT), a field he helped establish > through his research and service activities. His work has been funded > both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and > corporations (Intel, General Electric, Rockwell Collins, and United > Technologies) and has appeared in more than 70 refereed publications. He > is a founder and coordinator of the SMT-LIB initiative, an international > effort aimed at standardizing benchmarks and I/O formats for SMT > solvers. He has led the development of the award winning Darwin theorem > prover and the Kind model checker. He co-leads the development of CVC4,a > widely used and award winning SMT solver, and StarExec, a cross > community web-based service for the comparative evaluation of logic > solvers. From dbp at ccs.neu.edu Wed May 31 09:35:42 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Wed, 31 May 2017 09:35:42 -0400 Subject: [Pl-seminar] Reminder: Seminar TOMORROW: Cesare Tinelli, CoCoSpec: A Mode-aware Contract Language for Reactive Systems In-Reply-To: References: Message-ID: Reminder -- this is TOMORROW at 11AM. Daniel Patterson writes: > NUPRL Seminar presents > > Cesare Tinelli > University of Iowa > Host: Thomas Wahl > > 11AM-12:30PM (NOTE: THIS IS EARLIER THAN OUR NORMAL TIME!) > Thursday, June 1st, 2017 (NOTE: THIS IS NOT OUR STANDARD DAY OF WEEK!) > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > CoCoSpec: A Mode-aware Contract Language for Reactive Systems > > Abstract: > > Contract-based software development is a leading methodology for the > construction of safety- and mission-critical embedded systems. Contracts > are an effective way to establish boundaries between components and can > be used efficiently to verify global properties by using compositional > reasoning techniques. A contract specifies the assumptions a component > makes on its context and the guarantees it provides. Requirements in the > specification of a component are often case-based, with each case > describing what the component should do depending on a specific > situation (or mode) the component is in. > > This talk introduces CoCoSpec, a mode-aware assume-guarantee-based > contract language for embedded systems. CoCoSpec is built as an > extension of the Lustre language and lets users specify mode behavior > directly, instead of encoding it as conditional guarantees, thus > preventing a loss of mode-specific information. Mode-aware model > checkers supporting CoCoSpec can increase the effectiveness of the > compositional analysis techniques found in assume-guarantee frameworks > and improve scalability. Such tools can also produce much better > feedback during the verification process, as well as valuable > qualitative information on the contract itself. I will presents the > CoCoSpec language and illustrate the benefits of mode-aware > model-checking on a case study involving a flight-critical avionics > system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based > model checker developed at the University of Iowa that provides full > support for CoCoSpec. > > Bio: > > Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in > 1999 and is currently a professor in Computer Science at the University > of Iowa. His research interests include automated reasoning and formal > methods. He has done seminal work in automated reasoning, in particular > in Satisfiability Modulo Theories (SMT), a field he helped establish > through his research and service activities. His work has been funded > both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and > corporations (Intel, General Electric, Rockwell Collins, and United > Technologies) and has appeared in more than 70 refereed publications. He > is a founder and coordinator of the SMT-LIB initiative, an international > effort aimed at standardizing benchmarks and I/O formats for SMT > solvers. He has led the development of the award winning Darwin theorem > prover and the Kind model checker. He co-leads the development of CVC4,a > widely used and award winning SMT solver, and StarExec, a cross > community web-based service for the comparative evaluation of logic > solvers. From dbp at ccs.neu.edu Mon Jun 12 09:43:38 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Mon, 12 Jun 2017 09:43:38 -0400 Subject: [Pl-seminar] 6/23 Seminar: Dustin Jamner, Relational Parametricity for Polymorphic Blame Calculus Message-ID: NUPRL Seminar presents Dustin Jamner Northeastern University 12:00 Friday, June 23 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Relational Parametricity for Polymorphic Blame Calculus Abstract: The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this work we prove that the polymorphic blame calculus satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their concrete types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence. Bio: Dustin Jamner is an undergraduate at Northeastern University in Computer Science, working with Amal Ahmed. From dbp at ccs.neu.edu Wed Jun 21 04:57:54 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Wed, 21 Jun 2017 10:57:54 +0200 Subject: [Pl-seminar] Reminder: Seminar FRIDAY: Dustin Jamner, Relational Parametricity for Polymorphic Blame Calculus In-Reply-To: References: Message-ID: Hi all, Reminder that this seminar is on Friday, normal place & time. Daniel Patterson writes: > NUPRL Seminar presents > > Dustin Jamner > Northeastern University > > 12:00 > Friday, June 23 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Relational Parametricity for Polymorphic Blame Calculus > > Abstract: > > The polymorphic blame calculus integrates static typing, including > universal types, with dynamic typing. The primary challenge with this > integration is preserving parametricity: even dynamically-typed code > should satisfy it once it has been cast to a universal type. Ahmed et > al. (2011) employ runtime type generation in the polymorphic blame > calculus to preserve parametricity, but a proof that it does so has been > elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a > closely related system that combines ML and Scheme, but later found a > flaw in their proof. In this work we prove that the polymorphic blame > calculus satisfies relational parametricity. The proof relies on a > step-indexed Kripke logical relation. The step-indexing is required to > make the logical relation well-defined in the case for the dynamic type. > The possible worlds include the mapping of generated type names to their > concrete types and the mapping of type names to relations. We prove the > Fundamental Property of this logical relation and that it is sound with > respect to contextual equivalence. > > > Bio: > > Dustin Jamner is an undergraduate at Northeastern University in Computer > Science, working with Amal Ahmed. From types at ccs.neu.edu Tue Nov 21 13:40:58 2017 From: types at ccs.neu.edu (Benjamin Greenman) Date: Tue, 21 Nov 2017 13:40:58 -0500 Subject: [Pl-seminar] 12/5 Seminar: Fabian Muehlboeck: Efficient Nominal Gradual Typing Message-ID: NUPRL Seminar presents Fabian Muehlboeck Cornell University 1:30 Tuesday, December 5 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Efficient Nominal Gradual Typing Abstract: Recent research has identified significant performance hurdles that sound gradual typing needs to overcome. These performance hurdles stem from the fact that the run-time checks gradual type systems insert into code can cause significant overhead. We propose that designing a type system for a gradually typed language hand in hand with its implementation from scratch is a possible way around these and several other hurdles on the way to efficient sound gradual typing. Such a design process also highlights the type-system restrictions required for efficient composition with gradual typing. We formalize the core of a nominal object-oriented language that fulfills a variety of desirable properties for gradually typed languages, and present evidence that an implementation of this language suffers minimal overhead even in adversarial benchmarks identified in earlier work -------------- next part -------------- HTML attachment scrubbed and removed From types at ccs.neu.edu Wed Nov 22 14:53:39 2017 From: types at ccs.neu.edu (Benjamin Greenman) Date: Wed, 22 Nov 2017 14:53:39 -0500 Subject: [Pl-seminar] 12/5 Seminar: Fabian Muehlboeck: Efficient Nominal Gradual Typing In-Reply-To: References: Message-ID: TIME CHANGE: we'll start at 2:00pm instead of 1:30pm. Same date + location. On Tue, Nov 21, 2017 at 1:40 PM, Benjamin Greenman wrote: > NUPRL Seminar presents > > Fabian Muehlboeck > Cornell University > > 1:30 > Tuesday, December 5 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Efficient Nominal Gradual Typing > > Abstract: > > Recent research has identified significant performance hurdles that sound > gradual typing needs to overcome. These performance hurdles stem from the > fact that the run-time checks gradual type systems insert into code can > cause significant overhead. We propose that designing a type system for a > gradually typed language hand in hand with its implementation from scratch > is a possible way around these and several other hurdles on the way to > efficient sound gradual typing. Such a design process also highlights the > type-system restrictions required for efficient composition with gradual > typing. We formalize the core of a nominal object-oriented language that > fulfills a variety of desirable properties for gradually typed languages, > and present evidence that an implementation of this language suffers > minimal overhead even in adversarial benchmarks identified in earlier work > -------------- next part -------------- HTML attachment scrubbed and removed From types at ccs.neu.edu Mon Dec 4 10:59:22 2017 From: types at ccs.neu.edu (Benjamin Greenman) Date: Mon, 4 Dec 2017 10:59:22 -0500 Subject: [Pl-seminar] 12/5 Seminar: Fabian Muehlboeck: Efficient Nominal Gradual Typing In-Reply-To: References: Message-ID: Reminder: this is tomorrow at 2pm in WVH 366 On Wed, Nov 22, 2017 at 2:53 PM, Benjamin Greenman wrote: > TIME CHANGE: we'll start at 2:00pm instead of 1:30pm. > Same date + location. > > On Tue, Nov 21, 2017 at 1:40 PM, Benjamin Greenman > wrote: >> >> NUPRL Seminar presents >> >> Fabian Muehlboeck >> Cornell University >> >> 1:30 >> Tuesday, December 5 2017 >> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) >> >> Efficient Nominal Gradual Typing >> >> Abstract: >> >> Recent research has identified significant performance hurdles that sound >> gradual typing needs to overcome. These performance hurdles stem from the >> fact that the run-time checks gradual type systems insert into code can >> cause significant overhead. We propose that designing a type system for a >> gradually typed language hand in hand with its implementation from scratch >> is a possible way around these and several other hurdles on the way to >> efficient sound gradual typing. Such a design process also highlights the >> type-system restrictions required for efficient composition with gradual >> typing. We formalize the core of a nominal object-oriented language that >> fulfills a variety of desirable properties for gradually typed languages, >> and present evidence that an implementation of this language suffers minimal >> overhead even in adversarial benchmarks identified in earlier work > > From dbp at ccs.neu.edu Tue Dec 12 16:52:43 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Tue, 12 Dec 2017 16:52:43 -0500 Subject: [Pl-seminar] 12/14 Seminar: Molham Aref: Solver-Aided Declarative Programming Message-ID: <1513115563.1745868.1202986552.618EDEA2@webmail.messagingengine.com> NUPRL Seminar Presents Molham Aref Relational AI 10AM Thursday, December 14 2017 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) Solver-Aided Declarative Programming Abstract: I will summarize our work on a declarative programming language that offers native language support for model (or instance) finding. This capability can be used to express predictive (e.g. machine learning) and prescriptive (e.g. combinatorial optimization) analytics. The presentation gives an overview of the platform and the language. In particular, it focuses on the important role of integrity constraints, which are used not only for maintaining data integrity, but also, for the formal specification of complex optimization problems and probabilistic programming. Bio: Mr. Molham Aref is the Chief Executive Officer of Relational AI. Mr. Aref has more than 25 years of experience in developing and implementing enterprise-grade analytic, predictive, optimization and simulation solutions for the demand chain, supply chain, and revenue management across various industries. Relational AI combines the latest advances in Artificial Intelligence with a understanding of business processes to develop solutions that shape better decisions, improve agility, and reduce risk. Prior to Relational AI, he was co-founder and CEO of LogicBlox where he led the company from inception through a successful sale to Infor. Previously, he was CEO of Optimi (acquired by Ericsson), a leader in wireless network simulation and optimization, and co-founder of Brickstream (renamed Nomi and then acquired by FLIR), a leading provider of computer-vision-based behavior intelligence solutions. From dbp at ccs.neu.edu Wed Dec 13 16:18:56 2017 From: dbp at ccs.neu.edu (Daniel Patterson) Date: Wed, 13 Dec 2017 16:18:56 -0500 Subject: [Pl-seminar] 12/14 Seminar: Molham Aref: Solver-Aided Declarative Programming In-Reply-To: <1513115563.1745868.1202986552.618EDEA2@webmail.messagingengine.com> References: <1513115563.1745868.1202986552.618EDEA2@webmail.messagingengine.com> Message-ID: <87d13ie37j.fsf@dbpmail.net> Update: This has been moved to 108. Otherwise, same info! Daniel Patterson writes: > NUPRL Seminar Presents > > Molham Aref > Relational AI > > 10AM > Thursday, December 14 2017 > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > Solver-Aided Declarative Programming > > Abstract: > > I will summarize our work on a declarative programming language that > offers native language support for model (or instance) finding. This > capability can be used to express predictive (e.g. machine learning) and > prescriptive (e.g. combinatorial optimization) analytics. The > presentation gives an overview of the platform and the language. In > particular, it focuses on the important role of integrity constraints, > which are used not only for maintaining data integrity, but also, for > the formal specification of complex optimization problems and > probabilistic programming. > > > Bio: > > Mr. Molham Aref is the Chief Executive Officer of Relational AI. Mr. > Aref has more than 25 years of experience in developing and implementing > enterprise-grade analytic, predictive, optimization and simulation > solutions for the demand chain, supply chain, and revenue management > across various industries. Relational AI combines the latest advances in > Artificial Intelligence with a understanding of business processes to > develop solutions that shape better decisions, improve agility, and > reduce risk. Prior to Relational AI, he was co-founder and CEO of > LogicBlox where he led the company from inception through a successful > sale to Infor. Previously, he was CEO of Optimi (acquired by Ericsson), > a leader in wireless network simulation and optimization, and co-founder > of Brickstream (renamed Nomi and then acquired by FLIR), a leading > provider of computer-vision-based behavior intelligence solutions. From yee.mi at husky.neu.edu Thu Dec 14 09:59:36 2017 From: yee.mi at husky.neu.edu (Ming-Ho Yee) Date: Thu, 14 Dec 2017 09:59:36 -0500 Subject: [Pl-seminar] 12/14 Seminar: Molham Aref: Solver-Aided Declarative Programming In-Reply-To: <87d13ie37j.fsf@dbpmail.net> References: <1513115563.1745868.1202986552.618EDEA2@webmail.messagingengine.com> <87d13ie37j.fsf@dbpmail.net> Message-ID: Actually, we are in 110. There is an exam going on in 108, so don't go in! On Wed, Dec 13, 2017 at 4:18 PM, Daniel Patterson wrote: > Update: This has been moved to 108. Otherwise, same info! > > Daniel Patterson writes: > > > NUPRL Seminar Presents > > > > Molham Aref > > Relational AI > > > > 10AM > > Thursday, December 14 2017 > > Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) > > > > Solver-Aided Declarative Programming > > > > Abstract: > > > > I will summarize our work on a declarative programming language that > > offers native language support for model (or instance) finding. This > > capability can be used to express predictive (e.g. machine learning) and > > prescriptive (e.g. combinatorial optimization) analytics. The > > presentation gives an overview of the platform and the language. In > > particular, it focuses on the important role of integrity constraints, > > which are used not only for maintaining data integrity, but also, for > > the formal specification of complex optimization problems and > > probabilistic programming. > > > > > > Bio: > > > > Mr. Molham Aref is the Chief Executive Officer of Relational AI. Mr. > > Aref has more than 25 years of experience in developing and implementing > > enterprise-grade analytic, predictive, optimization and simulation > > solutions for the demand chain, supply chain, and revenue management > > across various industries. Relational AI combines the latest advances in > > Artificial Intelligence with a understanding of business processes to > > develop solutions that shape better decisions, improve agility, and > > reduce risk. Prior to Relational AI, he was co-founder and CEO of > > LogicBlox where he led the company from inception through a successful > > sale to Infor. Previously, he was CEO of Optimi (acquired by Ericsson), > > a leader in wireless network simulation and optimization, and co-founder > > of Brickstream (renamed Nomi and then acquired by FLIR), a leading > > provider of computer-vision-based behavior intelligence solutions. > > _______________________________________________ > pl-seminar mailing list > pl-seminar at lists.ccs.neu.edu > https://lists.ccs.neu.edu/bin/listinfo/pl-seminar > -------------- next part -------------- HTML attachment scrubbed and removed