headers
Daniel C. Wang | 1 Jan 2004 06:45
Picon

Sequent calculus and ANF

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Just wondering, but does anyone have pointers to literature that 
explicitly connect typed variants of Sabry and Felleisen's A-normal-form 
with sequent calculus style proof systems? The connection seems pretty 
direct and obvious, but I can't seem to find any reference that make 
this observation. Is this a case of the compiler writers and logician's 
simply not being aware of each others work?
Permalink | Reply | 0 comments |
headers
Daniel C. Wang | 1 Jan 2004 21:47
Picon

Re: Sequent calculus and ANF

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Ahh thanks to Matthias Blume for point me to the work by Ohori

Atsushi Ohori. A Curry-Howard isomorphism for compilation and program 
execution. Proc. TLCA Conference, Springer LNCS 1581, 258-179, April 1999.

   http://www.jaist.ac.jp/~ohori/research/anormal.pdf
Permalink | Reply | 1 comment |
headers
Frank Pfenning | 2 Jan 2004 17:42
Picon
Favicon

Re: Sequent calculus and ANF

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Hi Dan,

  as mentioned in the conclusion of Ohori's paper, it does not tell the
whole story.  There is also a connection between A-normal form, Moggi's
monadic meta-language, and lax logic.  This goes back to work by
[Benton, Biermann, and de Paiva'98], [Kobayashi'97] and, of
course, [Moggi'88,'89,'91].  You can read about that in:

Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal
logic. Mathematical Structures in Computer Science, 11:511-540,
2001. http://www.cs.cmu.edu/~fp/papers/mscs00.pdf

  - Frank

> Ahh thanks to Matthias Blume for point me to the work by Ohori
> 
> Atsushi Ohori. A Curry-Howard isomorphism for compilation and program 
> execution. Proc. TLCA Conference, Springer LNCS 1581, 258-179, April 1999.
> 
>    http://www.jaist.ac.jp/~ohori/research/anormal.pdf
Permalink | Reply | 0 comments |
headers
Jiri Adamek | 5 Jan 2004 14:00
Picon
Picon
Favicon

CMCS'04: deadline prolongation

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Excuse multiple copies
The deadline for submissions to CMCS 2004 has been prolonged to January
12. A copy of the second announcement follows:

+++++++++++++++++   SUBMISSION DEADLINE: JANUARY 12, 2004  +++++++++++++++

        +----------------------------------------------------------+
        |                                                          |
        |                                                          |
        |           7th International Workshop on                  |
        |       Coalgebraic Methods in Computer Science            |
        |                                                          |
        |                    C M C S  2004                         |
        |                                                          |
        |                                                          |
        |           Barcelona, March 27-29, 2004                   |
        |           http://www.iti.cs.tu-bs.de/~cmcs/		   |
        |                                                          |
        +----------------------------------------------------------+

The workshop is held in conjunction with

                ETAPS 2004 (7th European Joint Conferences on Theory
                Theory and Practice of Software, March 27- April 4,2004)
                http://www.lsi.upc.es/etaps04/

AIMS AND SCOPE
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carsten Schuermann | 5 Jan 2004 20:22
Picon
Favicon

CFP: LFM'04 - Logical Frameworks and Meta-languages

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

                    Fourth International Workshop on
                 Logical Frameworks and Meta-Languages
                                (LFM'04)

                 http://www.cs.yale.edu/~carsten/lfm04

                     A IJCAR'04 affiliated workshop
                   Cork, Ireland, July 04 - 08, 2004
		 http://4c.ucc.ie/ijcar/index.html

Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science.  Their
design and implementation has been the focus of considerable research
over the last two decades, using competing and sometimes incompatible
basic principles.

This workshop will bring together designers, implementors, and
practitioners to discuss all aspects of logical frameworks.  Topics
include, but are not limited to:

 - logical framework design
 - meta-theoretic analyses
 - applications and comparative studies
 - implementation techniques
 - efficient proof representation and validation
 - proof-generating decision procedures and theorem provers
 - proof-carrying code
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin C. Pierce | 7 Jan 2004 17:14

TYPES: Changing of the guard

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Dear Types readers,

The Types Forum is now more than a decade and a half old.  Begun by Albert
Meyer, it was carried through the early 1990s by Philip Wadler.  I've served
as moderator since 1996.

It's been a great time: the field of type systems (and programming languages
more generally) has matured and expanded in amazing ways, and the Types list
has helped provided cohesion and communication within the community as it
grew; list membership has ballooned from a couple hundred to over a
thousand.  I've had great fun and learned an enormous amount myself during
these years.  However, all things must change, and it is time now for me to
hand the baton to a new moderator.

It gives me great pleasure to introduce your new moderator, Stephanie
Weirich.  Stephanie is known to many of you already from her many research
contributions over the past several years, in particular her elegant work on
intensional type analysis.  I'm delighted to be leaving the list in such
capable and knowledgeable hands.

Though I won't be moderating Types, I will certainly still be reading it!
Good luck and best wishes to Stephanie.  Thank you all for your
contributions to Types, past and future, and I look forward to continuing
our work together in this most excellent area.

    - Benjamin  

P.S.  The handover of moderation will be accompanied by some modernization
(Continue reading)

Permalink | Reply | 1 comment |
headers
Stephanie Weirich | 7 Jan 2004 20:37
Favicon
Gravatar

Re: TYPES: Changing of the guard

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

First, I'm sure I speak for the whole community in
thanking Benjamin for the excellent job he has done
as TYPES moderator.

As Benjamin mentioned in the last email, we have switched the
management of the TYPES list to Mailman.

**** If you are currently subscribed and want to continue ******
**** reading and posting to TYPES, you do not need to     ******
**** change anything.

In particular, submission to TYPES is still the same, by sending
email to types@... More information about submitting to
TYPES can be found at the new web page:
    http://lists.seas.upenn.edu/mailman/listinfo/types-list

However, there are a few, hopefully positive, changes that have
resulted from the switch to Mailman:

* New headers for filtering types messages

   All email from TYPES will contain the string "[TYPES]" in the
   Subject header. Also, some of the headers may change with the new
   system, so if you are filtering TYPES email, you may have to update
   your rules. In particular, the first line of every TYPES email (see
   above) reflects the new address for the web pages.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Pieter Hartel | 11 Jan 2004 15:00
Picon
Picon
Picon

Vacancies Twente, The Netherlands

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

VACANCY NOTICE TWO POSTDOCS SECURITY

The Faculty of Electrical Engineering, Mathematics and Computer Science
(EEMCS) at the University of Twente in the Netherlands offers courses in
Electrical Engineering, Applied Mathematics, Computer Science,
Telematics, and Business Information Technology.

The Centre for Telematics and Information Technology (CTIT) is a
multi-disciplinary research institute of the University. CTIT
coordinates the research activities in all the areas relevant to the
development, the introduction and the usage of telematics and
information technology systems.

The Distributed and Embedded Systems Research (DIES) Group of EEMCS/CTIT
leads a multidisciplinary interest group in security research with
important contributions from the Faculty of Behavioural Sciences and the
Faculty of Business, Public Administration and Technology. DIES has
vacancies for two PostDocs:

1 PostDoc design and verification of cryptographic protocols

In the NWO project Account, which develops methods and tools to analyse
accountability in e-commerce protocols (see
http://dies.cs.utwente.nl/research/#account)

2 PostDoc security policies

In the European INSPIRED project, which develops the next generation
(Continue reading)

Permalink | Reply | 0 comments |
headers
Yukiyoshi Kameyama | 12 Jan 2004 16:38
Picon
Favicon

FLOPS 2004 Call for Participation

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

---------------------------------------------------------------------

                     Call for Participation

              The Seventh International Symposium 
                              on 
                Functional and Logic Programming
                          (FLOPS 2004)
                  Nara, Japan, April 7-9, 2004

================================
 Information
================================

  FLOPS Home        
       http://logic.is.tsukuba.ac.jp/flops2004/

  FLOPS local organization
       http://wwwfun.kurims.kyoto-u.ac.jp/flops2004/

  Sattelite Workshop: 
       Workshop on Algebra and Logic on Programming Systems (ALPS)
       April 10, 2004, Kyoto
       http://www.kurims.kyoto-u.ac.jp/~hassei/ALPS.html

================================
 Registration and Accommodation
================================
(Continue reading)

Permalink | Reply | 0 comments |
headers
Fausto Spoto | 12 Jan 2004 19:08
Picon

LOPSTR+PEPM+PPDP+SAS 2004: Last Call for Workshop Proposals

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

PLEASE ACCEPT MY APOLOGIES IF YOU RECEIVE THIS MESSAGE MORE THAN ONCE.

             LOPSTR'04 + PEPM'04 + PPDP'04 + SAS'04
              *** CALL FOR WORKSHOP PROPOSALS ***
              *** DEADLINE:  January 18, 2004 ***

             International Symposium on Logic-based
              Program Synthesis and Transformation
             URL: http://www.sci.univr.it/~lopstr04

           ACM SIGPLAN Symposium on Partial Evaluation
            and Semantics Based Program Manipulation
              URL: http://www.sci.univr.it/~pepm04

              ACM-SIGPLAN International Conference
      on Principles and Practice of Declarative Programming
              URL: http://www.sci.univr.it/~ppdp04

            International Static Analysis Symposium
              URL: http://www.sci.univr.it/~sas04

LOPSTR'04, the International Symposium on Logic-based Program
Synthesis and Transformation, PEPM'04, the ACM SIGPLAN 2004
Symposium on Partial Evaluation and Semantics Based Program
Manipulation, PPDP'04, the 6th ACM-SIGPLAN International
Conference on Principles and Practice of Declarative Programming,
and SAS'04, the 11th International Static Analysis Symposium, will
be held in Verona, Italy, from August 24 to August 28, 2004.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane