headers
Julian Rathke | 1 Jun 2004 17:45
Picon
Favicon

Workshop in Foundations of Global Computing

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

(n.b. submission date Monday 7th June, not 4th June as previous advertised)

                        **** CALL FOR PAPERS ****

                                FGUC'04

       3rd Joint Workshops on Foundations of Global Ubiquitous Computing
        and UK Grand Challenge in Science for Global Ubiquitous Computing.

                        The Royal Society, London, UK
                  Friday 3rd and Saturday 4th September, 2004.
                         Affiliated with CONCUR 2004

                      http://www.cogs.susx.ac.uk/fgc04/

IMPORTANT DATES:

  Deadline for submission:    Monday 7th June, 2004
  Notification of acceptance: Monday 5th July, 2004
  Final version due:          August, 2004
  FGUC'04 workshop:           Friday & Saturday 3rd-4th September, 2004

SCOPE:

The growing diffusion of large-scale networks of computing
devices of varying character and the concomitant services and
applications provided for such networks is promoting Global Ubiquitous
Computing (GUC) as an emerging model of computation. Processes and
(Continue reading)

Permalink | Reply | 0 comments |
headers
Hasegawa Masahito | 4 Jun 2004 11:18
Picon
Picon

TLCA 05 Call for Papers

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

                       Seventh International Conference on
               Typed Lambda Calculi and Applications (TLCA '05)
                                  Nara, Japan
                               21-23 April 2005
                        (Colocated with RTA as RDP '05)
                  http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/

The TLCA series of conferences serves as a forum for presenting original
research results that are broadly relevant to the theory and applications 
of typed lambda calculi and related systems. The following list of topics 
is non-exhaustive:

   * Typed and untyped lambda-calculi as models of computation.
   * Proof-theory: Natural deduction, sequent calculi, cut elimination
     and normalization. Propositions as types, linear logic and proof nets.
   * Types: Subtypes, dependent types, type inference, polymorphism, 
     types for security.
   * Semantics: Denotational semantics, game semantics, realizability,
     categorical models.
   * Programming languages: Foundations of functional and object-oriented
     programming, proof search, logic programming, type checking.
   * Implementation: Abstract machines, parallel execution, optimal
     reduction, program optimization.
   * Computer-aided reasoning.

The programme of TLCA'05 will consist of three invited talks and about 25 
papers selected from original contributions. Accepted papers will be published 
as a volume of Springer Lecture Notes in Computer Science series.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin Pierce | 5 Jun 2004 17:10
Favicon

Re: Type theory applications to the Semantic Web/RDF

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

>       For those of you familiar with XML (eXtended
> Markup Language) and Schemas, can you point me at
> papers that apply type theory (categorical perhaps) to
> XML and XML Schema? 

There are lots.  For example, check out the XDuce and Xtatic languages
designed at Penn

      http://www.cis.upenn.edu/~bcpierce/xduce
      http://www.cis.upenn.edu/~bcpierce/xtatic

and follow citations there (or go directly via Google) to papers on XQuery,
CDuce, Xact, Xen, RelaxNG, etc., etc.

Regards,

    - Benjamin

-----------------------------------------------------------------------------
BENJAMIN C. PIERCE, Professor                                               
Dept. of Computer & Information Science     
University of Pennsylvania                                    +1 215 898-2012
3330 Walnut St.                                          Fax: +1 215 898-0587
Philadelphia, PA 19104, USA                http://www.cis.upenn.edu/~bcpierce
-----------------------------------------------------------------------------
Permalink | Reply | 0 comments |
headers
Stephanie Weirich | 8 Jun 2004 21:15
Favicon
Gravatar

Logic Colloquium 2004 - Call for participation

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

CALL FOR PARTICIPATION - LC2004

Logic Colloquium 2004 (LC2004)
http://lc2004.unito.it/
(early registration deadline: 14th June 2004)
-------------------------------------------------------------

LC2004 is the annual meeting of the Association of Symbolic Logic, in 
fact the worldwide official congress dedicated
to the state-of-the-art of all branches of pure and applied logic.

LC2004 will be held in Torino, 25-31 July 2004. Conference themes 
encompass all aspects of symbolic logic and its applications,
including computer science. A special session, in the present year, will 
be devoted to devoted to universal algebra.

The deadline for early registration has been extended to June 14. Until 
that date you can still register to the LC2004 for 180 euro --- after 
that date the registration fee will be 230 euro.

Some info about the forthcoming conference (more may be found in the web 
page above):

Plenary speakers
John Baldwin
Tomek Bartoszynski
Alessandro Berarducci
Alberto Marcone
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alex Simpson | 10 Jun 2004 15:10
Picon
Picon
Favicon

LICS 2004 - Call for Participation

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

The deadline for early registration for LICS 2004 is *June 15, 2004*.

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

                        CALL FOR PARTICIPATION

                 Nineteenth Annual IEEE Symposium on 
                LOGIC IN COMPUTER SCIENCE (LICS 2004)

               July  13th - 17th, 2004, Turku, Finland
              http://www.lfcs.informatics.ed.ac.uk/lics/

The LICS Symposium is an annual international forum on theoretical and
practical topics in computer science that relate to logic in a broad
sense.

For registration visit

  http://www.math.utu.fi/ICALP04/registration.html

The deadline for early registration is June 15, 2004.

Collocated events: 
ICALP'04 will be collocated with LICS'04; for details see
http://www.math.utu.fi/ICALP04/. 

Invited Speakers:
The following distinguished speakers will give invited talks at LICS 2004:
(Continue reading)

Permalink | Reply | 0 comments |
headers
R. Ramanujam | 9 Jun 2004 10:48
Picon

FSTTCS 2004 Call for Papers

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

Dear Editor,

Please post the following CFP on the types list. The
conference typically gets many submissions in areas
like  polymorphic lambda calculus, type checking,
linear logic, full abstraction, domain theory, and
type systems for concurrent, distributed, and mobile
programming, so the announcement will surely interest
the TYPES readers.

Thanks, Ramanujam

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

                   FST&TCS 2004
               The 24th Conference on
        Foundations of Software Technology and
            Theoretical Computer Science

	        December 16--18, 2004,
	           Chennai, INDIA

	           CALL FOR PAPERS

* Important dates:
  Submissions:    21st June   2004
  Notification:   20th August 2004
(Continue reading)

Permalink | Reply | 0 comments |
headers
Francois Pottier | 9 Jun 2004 11:28
Picon
Picon
Favicon

Constraint-Based Type Inference for Guarded Algebraic Data Types

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

Hello all,

Vincent Simonet and I would like to announce the availability of the following
draft paper, which has been submitted to a journal. Comments of all kinds are
very much welcome.

  Title:
  Constraint-Based Type Inference for Guarded Algebraic Data Types

  URL:
  http://pauillac.inria.fr/~fpottier/publis/simonet-pottier-hmg.pdf

  Abstract:

  Guarded algebraic data types subsume the concepts known in the literature as
  indexed types, guarded recursive datatype constructors, and first-class
  phantom types, and are closely related to inductive types. They have the
  distinguishing feature that, when typechecking a function defined by cases,
  every branch may be checked under different typing assumptions. This mechanism
  allows exploiting the presence of dynamic tests in the code to produce extra
  static type information.

  We propose an extension of the constraint-based type system HM(X) with deep
  pattern matching, guarded algebraic data types, and polymorphic recursion. We
  prove that the type system is sound and that, provided recursive function
  definitions carry a type annotation, type inference may be reduced to
  constraint solving. Then, because solving arbitrary constraints is expensive,
  we further restrict the form of type annotations and prove that this allows
(Continue reading)

Permalink | Reply | 0 comments |
headers
slind | 9 Jun 2004 01:11
Picon
Favicon

TPHOLs: Call for participation

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

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

                  CALL FOR PARTICIPATION: TPHOLs 2004

                 The 17th International Conference on
                Theorem Proving in Higher Order Logics

                           Park City, Utah

              Tuesday 14 September - Friday 17 September 2004

              ***********************************************
              *     http://www.cs.utah.edu/tphols2004/      *
              ***********************************************

The 2004 International Conference on Theorem Proving in Higher Order
Logics will be the seventeenth in a series that dates back to 1988.
The conference will be held Tuesday September 14 through Friday
September 17 in Park City, Utah.

ACCEPTED PAPERS

    * Behzad Akbarpour and Sofiene Tahar
      Error Analysis of Digital Filters using Theorem Proving

    * Penny Anderson and Frank Pfenning
      Verifying Uniqueness in a Logical Framework
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean-Yves Marion | 9 Jun 2004 18:41
Picon
Favicon

Post-doc position in formal verification of computer systems - Loria

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

Post-doc position in formal verification of computer systems.
Loria – QSL group
France

Applications are invited for a Loria post-doctoral position from strong 
candidates working in formal methods, deductive or verification 
software.

The starting point is that for formal methods to be applied in 
practice, they must combine a high degree of automation with facilities 
for user interaction at a meaningful level of abstraction, and they 
must be cost-effective. The successful candidate will be expected to 
engage research in combinations of deductive or verification software. 
The goal is to provide for a language and a framework enabling 
developers to verify their designs using combinations of deductive 
tools. Comparable approaches include the SAL framework developed at 
SRI.
This position offers the oportunity to carry out research in both 
theoretical and practical aspects of formal methods.
The sucessful candidate will work at Loria in the QSL group, « Qualité 
et sûreté des logiciels ». Loria is one of the most important computer 
science laboratory in France, see www.loria.fr. The QSL group includes 
several research teams working on formal methods in computer science, 
see qsl.loria.fr.
Applicants should submit a curriculum-vitae, a statement of research 
and names of references.
The closing date for receipt of applications is 30 June 2004. Further 
details are available at qsl.loria.fr or by email request to
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carsten Schuermann | 15 Jun 2004 03:02
Picon
Favicon

Call for participation: LFM'04 - Logical Frameworks and Meta-languages

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

                    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 |

Gmane