CFP: 9th Intl. Workshop on Logic & Computational Complexity (LCC'07)

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

CALL FOR PAPERS: 9TH INTL WORKSHOP ON LOGIC AND COMPUTATIONAL COMPLEXITY
------------------------------------------------------------------------

   The Logic and Computational Complexity Workshop, LCC'07, will be
   held 15 July 2007 in Wroclaw, Poland as a satellite workshop of
   the Logic in Computer Science Conference (LICS'07).

SCOPE

   The workshop aims at furthering an understanding of the fundamental
   relations between computational complexity and logic.  Topics of
   interest include:

    * complexity analysis for functional languages
    * complexity in database theory
    * complexity in formal methods
    * complexity-theoretic type systems
    * computational complexity in higher types
    * formal methods for complexity analysis of programs
    * foundations of implicit computational complexity
    * logical & machine-independent characterizations of complexity  
classes
    * logics closely related to complexity classes
    * proof complexity
    * semantic approaches to complexity
    * software that applies LCC ideas

FORMAT

[TYPES/announce] DCM '07 Call for Papers

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

[TYPES/announce] Assoc. Professorship Opening

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

    Associate Professorship in 
    Programming, Logic and Semantics at the 
    IT University of Copenhagen, Denmark.

The IT University of Copenhagen invites applications for a position as
Associate Professor in the Programming, Logic, and Semantics Group.
The position is available from August 2007. 

The Programming, Logic and Semantics (PLS) group at the IT University of
Copenhagen conducts research in semantics of logics and programming
languages; models for concurrent, mobile and distributed systems; logical
frameworks, modular software verification; programming language
implementation techniques; program analysis; and programming language
technology for distributed and mobile applications, in particular for
context-aware mobile computing.

The successful candidate must document internationally recognized research
in the research areas of the PLS group. Moreover, the applicant should be
willing and able to teach in a wide variety of courses at all levels.

Please see
	http://www1.itu.dk/sw58262.asp

for the full official announcement.

Application deadline is April 16, 2007.

[TYPES/announce] EUROCORES Programme LogICCC - CfP

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

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

## Please feel free to circulate this message ##

Dear colleagues,

Following agreement with funding organisations in Austria, Belgium,
Croatia, Cyprus, Czech Republic, Denmark, Finland, France, Germany,
Israel, Netherlands, Portugal, Rumania, Spain, Sweden and Turkey, the
European Science Foundation is launching a Call for Outline Proposals
for Collaborative Research Projects to be undertaken within the
EUROCORES Programme “Modelling intelligent interaction - Logic in the
Humanities, Social and Computational sciences (LogICCC)”. The deadline
for Outline Proposals is 11 May 2007, 12:00 PM (noon).

The Call has been published on the ESF website at
http://www.esf.org/logic, where you will also find useful information on
the maximum number of individual projects that the participating funding
agencies are able to fund. For your convenience, these documents have
also been enclosed.

Please note that applicants should contact their national funding
agencies in order to verify their eligibility and to ensure compliance
with the relevant agencies’ current granting rules and regulations.
Contact details can be found in the Call for Proposals.

[TYPES/announce] TYPES 2007 remind

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

Dear All,
this is to gentle remind you that the deadline for (early)  
registration to TYPES is approaching (March 31).
And actually, hotels in Cividale have still a few free rooms left, so  
it would be a good idea to register and book your room as soon as  
possible.
More details on the web page http://www.dimi.uniud.it/types07

All the best
-Marino Miculan
TYPES 2007 organization committee

Request for Comments: Typing Functional Stack-Based Language

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

I'm writing to request comments on a technical report I've written
called: Typing Functional Stack-Based Languages.

==
Abstract

Stack-based languages have been in continuous use for approximately
four decades, and are still very popular today as intermediate
languages. Many of the most well-known stack-based languages (e.g.
Forth, Postscript, CIL, JVML) lack support for functional programming
at the primitive instruction level. Some notable exceptions are the
Joy programming language by Manfred von Thun and the Factor
programming language by Slava Pestov. There has also been a recent
proposal to add lambda expressions to Forth by Lynas and Stoddart.

While functional stack-based languages are gaining popularity, none of
these have a static type system. This paper addresses this gap by
formally expressing the operational semantics and type system for Cat,
a small functional stack-based language.
==

The rest of the article is available online at
http://www.cat-language.com/paper.html.

Any comments or suggestions would be greatly appreciated.

Thanks again to everyone who responded so generously to my previous
request for comments. I've incorporated many of the suggestions into

CFP: 2nd CFP for RDP Workshop Proof Assistants and Types in Education (PATE)

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

Second call for paper, the deadline for submission is april 1, 2007.

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

              Call for Papers

      RDP (RTA 07 + TLCA 07) Workshop PATE

     Proof Assistants and Types in Education

             June 25 2007

         http://www.rdp07.org/pate.html
=====================================================================

This workshop is supported by the EU Types Coordination Action.

The purpose of the workshop is to bring together
researchers and lecturers interested in applying
type theory and proof assistants in teaching.

Contributions are solicited in the following subject areas
and related topics:

- type theory as a language for (teaching) mathematics and programming;
- computer assisted informal reasoning;
- tools and languages for teaching math and logic;
- experience in using proof assistants in class.

Google Summer of Code

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

The FreeSoftware Initiative Japan(http://www.fsij.org/) is looking for
participants of Google Summer of Code(http://code.google.com/soc).
Proposed ideas (https://members.fsij.org/trac/soc2007/wiki/Ideas)
include developing automatic program verifier, and OCaml related projects.
We also accept proposals not directly related to proposed ideas.  If
your project is selected, you are paid 4500$ from Google.

Please read carefully http://code.google.com/soc/tos.html and
https://members.fsij.org/trac/soc2007/wiki/Ideas before submitting
your proposal.  Feel free to ask me if you have a question.

Project ideas are:

*Automatic program verifier

Develop an automatic program verifier with the following features.

   - Accept any programs in popular programing languages such as
C/Java/Ruby and so on.
   - Produce correct answers for programs in a practical subset of
the language.
   - Produce approximate answers for all programs in the language.
   - Performance is not a goal. It suffices to demonstrate its
capability to small code fragments. However, it must have modular
design to future improvement.

The project goal is intentionally vague so that we can accept projects
using wide range of methodologies.  It mainly aims formal verification

[TYPES/announce] Concur 2007 Final CFP

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

[TYPES/announce] Concur 2007 Final CFP

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