Daniele Gorla | 1 Jun 10:32 2007
Picon

[TYPES/announce] SecCo'07: deadline extended!

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Apologies for multiple copies!

          ----------------------------------------
         |                                        |
         |     5th International Workshop on      |
         |   Security  Issues  in  Concurrency    |
         |                                        |
         |              (SecCo'07)                |
         |                                        |
          ----------------------------------------
         |                                        |
         | September 3rd, 2007, Lisboa (Portugal) |
         |       Affiliated to CONCUR 2007        |
         |                                        |
          ----------------------------------------

New submission deadlines:

           Submission of abstracts: June 4th, 2007
           Submission of papers: June 7th, 2007

For more details, see the web-page:

           http://www.dsi.uniroma1.it/~gorla/SecCo07/

Carlos Areces | 1 Jun 16:45 2007
Picon

[TYPES/announce] ESSLLI 2008: Call for Course and Workshop Proposals

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   20th European Summer School in Logic, Language and Information
                                 ESSLLI 2008
             Monday, 4 August - Friday, 15 August 2008
             Hamburg, Germany

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

                  CALL FOR COURSE and WORKSHOP PROPOSALS
                  --------------------------------------

The European Summer School in Logic, Language and Information (ESSLLI)
is organized every year by the Association for Logic, Language and
Information (FoLLI, http://www.folli.org) in different sites around
Europe.

The main focus of ESSLLI is on the interface between linguistics,
logic and computation.  ESSLLI offers foundational, introductory and
advanced courses, as well as workshops, covering a wide variety of
topics within the three areas of interest: Language and Computation,
Language and Logic, and Logic and Computation.

Previous summer schools have been highly successful, attracting up to
500 students from Europe and elsewhere.  The school has developed into
an important meeting place and forum for discussion for students and
researchers interested in the interdisciplinary study of Logic,
Language and Information.
(Continue reading)

Vasco Vasconcelos | 5 Jun 09:54 2007
Picon

[TYPES/announce] The AITO Dahl-Nygaard Prize Winners for 2007

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


AITO is very proud to announce that the Dahl-Nygaard Prizes for 2007 will be given to Luca Cardelli, Microsoft Research Cambridge (Senior prize) for his overall contribution to both theory and practice for object-oriented languages, and to Jonathan Aldrich, Carnegie Mellon University Pittsburgh (Junior prize) for his recent contribution to expressing and verifying software architecture in object-oriented languages.

Luca Cardelli systematically developed typing theories for objects, from record types to bounded quantification, eventually leading to the famous book "A Theory of Objects", published with Martin Abadi in 1996. This masterpiece develops an "object calculus" as a foundation for object-oriented languages, in much the same way that Church's lambda-calculus is a foundation for procedural languages. Overall, Luca's work was inspired by strong expertise on language design, including functional languages and theory, such as ML, and object-oriented languages such as Modula-3. This leads Luca to further contribute to language design in the domain of mobility and locality with contributions such as Obliq and Ambient. The Ambient Calculus (developed with Andy Gordon) enables the formal analysis of mobile and wide-area systems, in part by taking advantage of a decade of previous work on process algebra. This work on mobility indirectly led to his recent interest in Systems Biology.

Jonathan Aldrich develops lightweight ways to statically assure architectural characteristics of large, real-world object-oriented systems. His pioneering thesis work on ArchJava (with advisors Craig Chambers and David Notkin) was the first system to verify at compile time that the dynamic structure of an object-oriented application conforms to an abstract, hierarchical software architecture. ArchJava, like Jonathan's other work, tackles head-on challenging aspects of object-oriented systems, including aliasing, reentrancy, inheritance, and the use of sophisticated design patterns. Jonathan's research is grounded in formal soundness proofs yet is validated through case study evaluations with realistic software systems and tasks. More recently, Jonathan and his students have made contributions in other aspects of object-oriented architecture assurance, including object protocol checking, modularity in aspect-oriented programming, and novel object models.

The AITO Dahl-Nygaard Prizes are named for Ole-Johan Dahl and Kristen Nygaard, two pioneers in the area of programming and simulation. Their foundational work on object-oriented programming, made concrete in the Simula language, is one of the most important inventions in software engineering. Their key ideas were expressed already around 1965, but took over 20 years to be absorbed and appreciated by the broader software community. After that, object-orientation has profoundly transformed the landscape of software design and development techniques.

It was a great loss to our community that both Ole-Johan Dahl and Kristen Nygaard passed away in 2002. In remembrance of their scholarship and enthusiastic encouragement of young researchers, AITO has established in 2004 a prize to be awarded annually to a senior researcher with outstanding career contributions and a younger researcher who has demonstrated great potential for following in the footsteps of these pioneers. For 2006, the prize committee has recommended deviating from the norm and giving one prize but to a group of four people.

The prizes will be awarded in July at ECOOP 2007, July 30 - August 03, Berlin, Germany. Luca Cardelli and Jonathan Aldrich have agreed to give keynotes talks. For details, see the conference program.

David Naumann | 6 Jun 18:18 2007

Re: Formal proof of type-soundness for references in Coq

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Fri, 9 Feb 2007, mulhern wrote:
> Date: Fri, 9 Feb 2007 21:16:37 -0600
> From: mulhern <mulhern@...>
> To: types-list@..., coq-club@...
> Subject: [TYPES] Formal proof of type-soundness for references in Coq
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi!
>
> I've posted a formal proof in Coq of type-soundness for references at
> http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html.
>
> I think it might be interesting to people on the Coq list because it uses
> the module system.
>
> As far as I know, there is no other publicly available formal proof of
> type-soundness for references available, so it might be interesting to
> people on the types list as well.
>
> -mulhern

There was a follow-up clarifying Mulhern's interest in proof fragments,
and one from Crary on the formalization of Standard ML in POPL07.

For the record, there's other machine-checked work on languages with 
references, e.g., Nipkow's group has done type soundness for a fragment of 
Java using Isabelle/HOL.
(Continue reading)

David Hopwood | 7 Jun 00:31 2007
Picon

Re: Formal proof of type-soundness for references in Coq

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

David Naumann wrote:
> [Corejml 06]
> title={Preliminary Definition of Core {JML}},
> author={Gary T. Leavens and David A. Naumann and Stan Rosenberg},
> institition={Stevens Institute of Technology},
> number={CS Report 2006-07},
> URL={http://www.cs.stevens.edu/~naumann/SIT-TR-2006-07a.pdf}

Should be
<http://www.cs.stevens.edu/~naumann/publications/SIT-TR-2006-07.pdf>.

--

-- 
David Hopwood <david.hopwood@...>

benhamou | 17 Jun 17:47 2007
Picon

[TYPES/announce] Reminder: CFP of SymCon'07

[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We apologize for multiple copies of this Call.

================================================================

                         Call for Papers

                  SymCon'07

           The Seventh International Workshop
       on Symmetry and Constraint Satisfaction Problems
          (http://www.cmi.univ-mrs.fr/~benhamou/symcon07/)

      To be held at the Thirteenth International Conference
    on Principles and Practice of Constraint Programming (CP 2007)

                  Providence, RI, USA
              September 23rd 2007

================================================================

WORKSHOP DESCRIPTION
--------------------

SymCon'07 is the 7th in a series of workshops affiliated with the CP
conference, and focuses on the investigation of symmetry and symmetry
breaking techniques for Constraint Satisfaction Problems (CSPs).
Symmetries occur frequently in CSPs.  When undetected, they cause
(Continue reading)

N V Krishna. | 21 Jun 06:27 2007

Compiler frameworks.

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello All,
I am trying to make a compendium of different compiler frameworks that
are available. The frameworks can cater to any aspect of compiling
(Parsing / analysis / verification/ optimization/ code generation).
The problem is that of plenty. Each framework caters to different
needs, but there does not seem to be a single listing of all, possibly
with details on what the framework provides and still better with
comparisions with other similar ones. Many a times this leads to new
researchers either (a) using some
not-so-suitable-for-his-or-her-purpose framework or (b) coming up with
new frameworks.

I propose to making a public webpage, where all such frameworks can be
listed (If, some such page already exists, then please inform me). I
would be greatful, if each one of you, could take a few minutes and
write about (a) the compiler frameworks that you might have
developed/used and optionally (b) any comments you have about the
framework(s) (+/-).

On my part, I promise to compile this webpage and make it public.

Warm regards,
N V Krishna.

Eric Eide | 21 Jun 16:03 2007
Picon

Re: Compiler frameworks.

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

N V Krishna <nvk@...> writes:

	> I am trying to make a compendium of different compiler frameworks
	> that are available.  The frameworks can cater to any aspect of
	> compiling (Parsing / analysis / verification/ optimization/ code
	> generation).  The problem is that of plenty.  Each framework caters
	> to different needs, but there does not seem to be a single listing of
	> all, [...]

You might want to look at the "catalog of free compilers" and the "directory of
commercial compiler tools" that are associated with the `comp.compilers' USENET
newsgroup.

	<http://www.idiom.com/free-compilers/>
	<http://compilers.iecc.com/tools.html>
	<http://compilers.iecc.com/>

The catalogs are a bit dated, but perhaps better than starting from scratch.

Good luck ---

Eric.

--

-- 
-------------------------------------------------------------------------------
Eric Eide <eeide@...>  .         University of Utah School of Computing
http://www.cs.utah.edu/~eeide/ . +1 (801) 585-5512 voice, +1 (801) 581-5843 FAX

(Continue reading)

Aaron Gray | 23 Jun 17:08 2007
Picon

Re: Compiler frameworks.

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

>[ The Types Forum, 
>http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hello All,
> I am trying to make a compendium of different compiler frameworks that
> are available. The frameworks can cater to any aspect of compiling
> (Parsing / analysis / verification/ optimization/ code generation).
> The problem is that of plenty. Each framework caters to different
> needs, but there does not seem to be a single listing of all, possibly
> with details on what the framework provides and still better with
> comparisions with other similar ones. Many a times this leads to new
> researchers either (a) using some
> not-so-suitable-for-his-or-her-purpose framework or (b) coming up with
> new frameworks.
>
> I propose to making a public webpage, where all such frameworks can be
> listed (If, some such page already exists, then please inform me). I
> would be greatful, if each one of you, could take a few minutes and
> write about (a) the compiler frameworks that you might have
> developed/used and optionally (b) any comments you have about the
> framework(s) (+/-).
>
> On my part, I promise to compile this webpage and make it public.

You can add 'Prop' :-

        http://prop-cc.sourceforge.net/leunga/www/prop.html

(Continue reading)


Gmane