[TYPES/announce] The AVISPA Tool - v1.1

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

			   
[We apologize if you received multiple copies of this message]

             XXX   X     X  XXXXX   XXXXX  XXXXXX    XXX
            X   X  X     X    X    X     X X     X  X   X
           X     X X     X    X    X       X     X X     X
           X     X  X   X     X    X       X     X X     X
           XXXXXXX  X   X     X     XXXXX  XXXXXX  XXXXXXX
           X     X   X X      X          X X       X     X
           X     X   X X      X          X X       X     X
           X     X    X       X    X     X X       X     X
           X     X    X     XXXXX   XXXXX  X       X     X

                         V E R S I O N    1 . 1

                            (June 30, 2006)

We are happy to announce the availability of a new version of the
AVISPA Tool, a push-button tool for the Automatic Validation of
Internet Security-sensitive Protocols and Applications.  The AVISPA
Tool v1.1 is available at

                      http://www.avispa-project.org

The AVISPA Tool v1.1 includes several bug fixes and extends the

[TYPES/announce] Symposium for Gordon Plotkin: Call for Participation

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

                    SYMPOSIUM FOR GORDON PLOTKIN

                        7-8 September, 2006
         LFCS, School of Informatics, University of Edinburgh

    A symposium to celebrate the 60th birthday of Gordon Plotkin

         http://www.lfcs.ed.ac.uk/events/plotkin-symposium/

                      CALL FOR PARTICIPATION

PROGRAMME: Two days of invited talks on 7th and 8th September, with a
banquet on the evening of Thursday 7th September.

INVITED SPEAKERS: Martin Abadi (UC Santa Cruz); Samson Abramsky
(University of Oxford); Rod Burstall (University of Edinburgh,
Emeritus); Luca Cardelli (Microsoft Research, Cambridge); Marcelo Fiore
(University of Cambridge); Philippa Gardner (Imperial College);
Matthew Hennessy (University of Sussex); Robin Milner (Univerity of
Cambridge, Emeritus); Eugenio Moggi (Universita` di Genova);
John Power (University of Edinburgh); David Pym (Hewlett-Packard
Laboratories, Bristol); Dana Scott (Carnegie Mellon University,
Emeritus); Colin Stirling (University of Edinburgh); Glynn Winskel
(University of Cambridge).

SUPPORT FOR PHD STUDENTS: Financial assistance is available for
UK-based PhD students who wish to attend the symposium. This will

[TYPES/announce] SSS 2006 ---- Deadline extended to July 12

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

Systematically testing type systems

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

Hi all,

I hope this is not a stupid question, but I wonder whether it is feasible to 
test the soundness of a type checker by enumerating all programs in the 
language, reducing each program one step (assuming we have a small-step 
interpreter and a language where the full execution state is in the program 
itself) and checking whether subject reduction holds. If the enumeration of all 
programs would be smart enough (i.e., produce only syntactically correct 
programs; no two programs in the enumeration are alpha-equivalent) I could 
imagine that it would be feasible to test a type checker for all programs less 
than X bytes in size, where X is a reasonable number (e.g., 1KB) - at least for 
minimalistic languages as they are common in type research.

Has this ever been tried, or is it obvious that it would not work in practice?

Klaus Ostermann

Re: Systematically testing type systems

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

On Jul 4, 2006, at 6:13 AM, Klaus Ostermann wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Hi all,
>
> I hope this is not a stupid question, but I wonder whether it is  
> feasible to
> test the soundness of a type checker by enumerating all programs in  
> the
> language, reducing each program one step (assuming we have a small- 
> step
> interpreter and a language where the full execution state is in the  
> program
> itself) and checking whether subject reduction holds. If the  
> enumeration of all
> programs would be smart enough (i.e., produce only syntactically  
> correct
> programs; no two programs in the enumeration are alpha-equivalent)  
> I could
> imagine that it would be feasible to test a type checker for all  
> programs less
> than X bytes in size, where X is a reasonable number (e.g., 1KB) -  
> at least for
> minimalistic languages as they are common in type research.
>
> Has this ever been tried, or is it obvious that it would not work  

Re: Systematically testing type systems

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

This is not difficult to do in a logic programming language that supports
higher-order or nominal abstract syntax, such as lambdaProlog, Twelf, or
alphaProlog, using "generate-and-test"; the tricky part is getting the tests
right and setting up the search in such a way that you don't miss obvious
short counterexamples yet still terminate in a small amount of time (my
boredom threshold is five seconds).  Automated assertion checking has also
been investigated in a general (constraint) logic programming and in Haskell
(QuickCheck).  I'm not aware of any prior research on applying this idea
specifically to type systems.

Coincidentally, I wrote a short (and very very preliminary) paper on doing
this in alphaProlog for the upcoming Workshop on Mechanizing Metatheory;
this seems like as good a time as any to mention it.  It is not clear to me
how far an exhaustive search approach can be pushed, since the number of
well-typed programs of size n is still exponential in n; something like
QuickCheck's random checking, but guided by the type system and operational
semantics, might be a better way.  However, even doing an exhaustive search
for "small" counterexamples seems likely to be helpful, at least as a sanity
check for trivial bugs.

If you want to have a look at the paper draft, it's online at

http://homepages.inf.ed.ac.uk/jcheney/publications/wmm06-draft.pdf

Big caveat: alphaProlog is not that well supported right now and the code
for automatic checking is not in a public release yet.

Questions, comments, and fisticuffs welcome.

Re: Systematically testing type systems

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

Klaus Ostermann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi all,
> 
> I hope this is not a stupid question, but I wonder whether it is feasible to 
> test the soundness of a type checker by enumerating all programs in the 
> language, reducing each program one step (assuming we have a small-step 
> interpreter and a language where the full execution state is in the program 
> itself) and checking whether subject reduction holds. If the enumeration of all 
> programs would be smart enough (i.e., produce only syntactically correct 
> programs; no two programs in the enumeration are alpha-equivalent) I could 
> imagine that it would be feasible to test a type checker for all programs less 
> than X bytes in size, where X is a reasonable number (e.g., 1KB) - at least for 
> minimalistic languages as they are common in type research.
> 
> Has this ever been tried, or is it obvious that it would not work in practice?

It is obvious that it would not work in practice for programs up to 1 Kbyte.
It could only work for programs up to a few tokens in length.

--

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

[TYPES/announce] SOS 2006 - Programme and Call for Participation

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

CALL FOR PARTICIPATION:

     Structural Operational Semantics 2006

     - a satellite workshop of CONCUR 2006

     26th August 2006, Bonn (Germany)

     http://www.cse.unsw.edu.au/~rvg/SOS2006/

     !!! Early registration until 18th July !!!

INVITED SPEAKERS:

     Bartek Klin (Warsaw, PL)

     Robin Milner (Cambridge, UK) - joint Express-Infinity-SOS talk

PROGRAMME:

     09:00 Registration
     09:15 Welcome
     09:30 Bartek Klin (invited talk):
           Bialgebraic methods in structural operational semantics
     10:30 break
     11:00 MohammadReza Mousavi, Michel A. Reniers:
           On well-foundedness and expressiveness of promoted tyft

[TYPES/announce] Preliminary program for LCC'06

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

The following is a preliminary program for LCC'06 (the 2006 Workshop
on Logic and Computational Complexity) which is part of FLoC 2006
(the Federated Logic Conference).

The deadline for early registration for LCC'06 and FLoC 2006 is
**Monday, July 10**.  See http://www.easychair.org/FLoC-06/ for
on-line registration.

For updates on this prelimary program, check
              http://www.easychair.org/FLoC-06/LCC.html

====================================================================
LCC'06 PRELIMINARY PROGRAM

                        Thursday, August 10th

SESSION 1:   INVITED TALK

09:30-10:30  TBA

10:30-11:00  Break

SESSION 2:   CONTRIBUTED TALKS

11:00-11:45  Patrick Baillot, Ugo Dal Lago and Jean-Yves Moyen
                On Quasi-Interpretations, Blind Abstractions and
                Implicit Complexity

[TYPES/announce] Algebraic Theory of Automata and Logic Workshop CALL FOR PAPERS

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

**********************************************************************
*                Algebraic Theory of Automata and Logic              *
*                Satellite workshop of the conference CSL 06         *
*             September 30 -- October 1, 2006, Szeged, Hungary       *
*                Supported by the AUTOMATHA project of ESF           *
*                http://www.inf.u-szeged.hu/~csl06/ws.php            *
*                         CALL FOR PAPERS                            *
**********************************************************************

Organizers: Z. Ésik, H. Straubing, P. Weil, Th. Wilke

The aim of the workshop is to provide a forum for researchers interested
in the structure theory of automata and/or the application of the
algebraic approach to logic to present their results and to combine
their efforts in the further development of the structure theory of
finite automata, tree automata and related structures in connection with
formal logic.

The scientific program will consist of invited lectures and contributed
talks. It is also intend to leave some room for discussions (open
problem session, etc.). It is expected that some Ph. D. students will
also attend the meeting.

Abstracts of contributed talks must be sent by e-mail to Prof. Zoltan
Esik, ze@... The abstract should be of no more than two 
pages. The submission deadline is 20 July, 2006. Notifications of
acceptance will be sent by 30 July, 2006. We will announce the titles of