[PRL] [Pl-seminar] Grigore Rosu's visit -- early announcement

[Christos Dimoulas]

Here is a preliminary schedule for Grigore's visit.

Let me know if there are any conflicts or if someone requested for a 
meeting and his/her name does not show up.

Thanks.

Schedule November 16
--------------------
--------------------

09:15 -- 10:15 : Breakfast at Collonade (Christos Dimoulas)
10:30 -- 11:00 : David Van Horn
11:00 -- 11:30 : Amal Ahmed
11:45 -- 13:30 : Talk
13:30 -- 14:30 : Lunch (Jesse Tov, Amal Ahmed, Matthias Felleisen)
14:30 -- 15:00 : Pete Manolios
15:00 -- 15:30 : Matthias Felleisen
15:30 -- 16:00 : Stevie Strickland
16:00 -- 16:30 : Carl Eastlund
16:30 -- 17:00 : Thomas Wahl
17:00 -- 17:30 : Vincent St-Amour
17:30 -- 18:00 : Asumu Takikawa
18:00 -- 18:30 : Aaron Turon
18:30 -- 19:00 : Stephen Chang
19:00 --       : Dinner (David Van Horn, Thomas Wahl, Olin Shivers, 
Christos Dimoulas)



On 11/10/11 1:01 PM, Christos Dimoulas wrote:
> Next week we have Grigore Rosu (UIUC) visiting.
>
> Grigore will spend next Wednesday (November 16) at our lab. There are
> still some open slots for meetings. Let me know if you are interested.
>
> Here is the info of the talk and a short bio of the speaker:
>
> NEU Programming Languages Seminar presents
>
> Grigore Rosu
> Formal Systems Laboratory (FSL)
> Department of Computer Science
> University of Illinois at Urbana-Champaign
>
> Wednesday, 11/16
>
> 11:45am - 1:30pm
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
>
>
> Title: K and Matching Logic
>
> Abstract:: Would you like to wake up some morning, have a coffee, then
> design a non-trivial programming language, say with multidimensional
> arrays and array references, with functions and references to them, with
> blocks and local declarations, with input/output, with exceptions, with
> nondeterminism and concurrency with synchronization, and so on, and by
> evening to have a reasonably efficient interpreter, a state-space search
> tool and a model checker, as well as a deductive program verifier for
> your language, all correct-by-construction? Then you may be interested
> in K and Matching Logic, because that is what they are aiming for. K is
> a rewrite-based framework for defining formal operational semantics of
> programming languages. A K semantics can be executed, and thus tested,
> as if it was an interpreter for the defined language. This way, we can
> gain confidence in the correctness of our semantics. Then we can use
> precisely that semantics, unchanged, for program analysis and
> verification, without a need to give the language another, e.g.,
> axiomatic or denotational or dynamic, semantics. Matching logic consists
> of a language-independent proof system that allows us to reason about
> programs in any language that is given a rewrite-based operational
> semantics.
>
> Bio: Grigore Rosu is an associate professor in the Department of
> Computer Science at the University of Illinois at Urbana-Champaign
> (UIUC), where he leads the Formal Systems Laboratory (FSL). His research
> interests encompass both theoretical foundations and system development
> in the areas of formal methods, software engineering and programming
> languages. Before joining UIUC in 2002, he was a research scientist at
> NASA Ames. He obtained his Ph.D. at the University of California at San
> Diego in 2000 and his M.S. at the University of Bucharest, Romania, in
> 1996. He was offered the CAREER award by the NSF and the outstanding
> junior award by the Computer Science Department at UIUC in 2005. He won
> an ACM SIGSOFT distinguished paper award at ASE 2008 and the best
> software science paper award at ETAPS 2002. He was ranked a UIUC
> excellent teacher in Spring 2008 and Fall 2004.
>
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar