headers
gmh | 3 Mar 2000 09:34
Picon

Haskell Workshop

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

                      ANNOUNCEMENT AND CALL FOR PAPERS

                              Haskell Workshop

                    Montreal, Canada, 17th September 2000

     The Haskell Workshop forms part of the PLI 2000 colloquium on
     Principles, Logics, and Implementations of high-level programming
     languages, which comprises the ICFP and PPDP conferences, together
     with associated workshops.  Previous Haskell Workshops have been
     held in La Jolla (1995), Amsterdam (1997), and Paris (1999).

                  www.cs.nott.ac.uk/~gmh/hw00.{html,ps,txt}

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

SCOPE

The purpose of the Haskell Workshop is to discuss experience with Haskell,
and possible future developments for the language.  The scope of the
workshop includes all aspects of the design, semantics, theory, application,
implementation, and teaching of Haskell.  Submissions that discuss
limitations of Haskell at present and/or propose new ideas for future
versions of Haskell are particularly encouraged.

SUBMISSION DETAILS

   Deadline for submission:      1st June 2000
(Continue reading)

Permalink | Reply | 0 comments |
headers
Francis Tang | 3 Mar 2000 12:47
Picon
Picon

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover

Dear all,

I would like to draw your attention to the following preprint
available from http://www.dcs.ed.ac.uk/home/fhlt/Research/

Comments and suggestions are very welcome!

Yours faithfully,

Francis.

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem
Prover

          by Martin Hofmann and Francis Tang

We present an implementation of a program logic of objects, extending that
of Abadi and Leino. In particular, the implementation uses higher-order
abstract syntax (HOAS) and---unlike previous approaches using HOAS---at
the same time uses the built-in higher-order logic of the theorem prover
to formulate specifications. We give examples of verifications that have
been attempted with the implementation. Due to the mixing of HOAS and
built-in logic the soundness of the encoding is nontrivial and is
established by way of a semantic interpretation based on ideas from
category theory. The details of this interpretation will be given
elsewhere.

--
Francis Tang                       Email: francis.tang@...
LFCS, Division of Informatics,     Url: http://www.dcs.ed.ac.uk/~fhlt/
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ruy de Queiroz | 3 Mar 2000 16:26
Picon

7th WoLLIC'2000

                         Call for Contributions

        7th Workshop on Logic, Language, Information and Computation
       	                      (WoLLIC'2000)
                            August 15-18, 2000

 !  TUTORIALS   >>     (Tutorial Day: August 15th)       <<   TUTORIALS !

                            Natal, Brazil

The "7th Workshop on Logic, Language, Information and Computation"
(WoLLIC'2000), the seventh version of a series of workshops which started
in 1994 with the aim of fostering interdisciplinary research in pure and
applied logic, will be held in Natal, Brazil, from August 15th to 18th 2000.
Contributions are invited in the form of short papers (10 A4 10pt pages) in
all areas related to logic, language, information and computation, including:
pure logical systems, proof theory, model theory, algebraic logic, type theory,
category theory, constructive mathematics, lambda and combinatorial calculi,
program logic and program semantics, logics and models of concurrency,
logic and complexity theory, nonclassical logics, nonmonotonic logic,
logic and language, discourse representation, logic and artificial
intelligence, automated deduction, foundations of logic programming,
logic and computation, and logic engineering.

The 7th WoLLIC'2000 has the scientific sponsorship of the Association
for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics
(IGPL), the European Association for Logic, Language and Information (FoLLI),
the Sociedade Brasileira de Computacao (SBC), and the Sociedade Brasileira
de Logica (SBL).
(Continue reading)

Permalink | Reply | 0 comments |
headers
N. Yoshida | 3 Mar 2000 23:58
Picon
Picon
Favicon

Paper Announcement: Secure Information Flow as Typed Process Behaviour

We are pleased to announce the following paper:

         Secure Information Flow as Typed Process Behaviour                    

                                by 
          Kohei Honda    Vasco Vasconcelos   Nobuko Yoshida 

* Long version: - Queen Mary and Westfield College, CS Technical Paper 767
                - University of Leicester, MCS Technical Paper, 1/2000
* Short version: a revised version will appear in ESOP 2000, LNCS, Springer

are available from:

   http://www.dcs.qmw.ac.uk/~kohei              (Queen Mary and Westfield College)
   http://www.di.fc.ul.pt/~vv/publications.html (Lisbon University)
   http://www.mcs.le.ac.uk/~nyoshida/paper.html (Leicester University)

Your comments are warmly welcome. 

Kohei Honda:       Queen Mary and Westfield College,  kohei@...
Vasco Vasconcelos: University of Lisbon,              vv@...
Nobuko Yoshida:    University of Leicester,           ny11@...

----------------------------- ABSTRACT ------------------------------
We propose a new type discipline for the $\pi$-calculus in which
secure information flow is guaranteed by static type checking.
Secrecy levels are assigned to channels and are controlled by
subtyping.  A behavioural notion of types capturing causality of
actions plays an essential role for ensuring safe information flow in
diverse interactive behaviours, making the calculus powerful enough to
(Continue reading)

Permalink | Reply | 0 comments |
headers
Doris Faehndrich | 6 Mar 2000 18:41
Picon

ETAPS 2000 - 2nd Call for Participation

(Sorry, if you receive multiple copies of this Call.
                                       Doris Faehndrich)
------------------------------------------------------------------
ETAPS 2000 - EUROPEAN JOINT CONFERENCES ON
                       THEORY AND PRACTICE OF SOFTWARE

      Technical University of Berlin, March 25 - April 2, 2000

-------- CALL FOR PARTICIPATION ----- REMINDER -------------------

Welcome to Berlin, welcome to ETAPS, the European Joint Conferences on 
Theory and Practice of Software, the European forum for academic and 
industrial researchers working on these topics!  

For 9 days you will be able to choose between 
5 conferences -TACAS 2000, FOSSACS 2000, FASE 2000, ESOP 2000, 
    CC 2000 - with more than 120 regular papers and tool 
    demonstrations  covering a wide range of topics from theory 
    and practice,  
7 invited lectures by Abbas Edalat, David Harel, Martin Odersky, 
    Richard M. Soley, Wlayslaw M. Turski, Reinhard Wilhelm, Pierre
    Wolper, 
5 satellite events - GRATRA 2000, CMCS 2000, CBS 2000, INT 2000,
    CoFi 2000 -,
10 tutorials - XML for Software Engineers, A tutorial on Maude,
    Rigorous Requirements for Safety-Critical Systems: Fundamentals 
    and Applications of the SCR Method, Multi-Paradigm Programming,
    Query-based Automated Debugging, The Unified Modelling Language,
    Swinging Types, Tables and computation, SDL 2000, Software 
    Metrology Basis -
(Continue reading)

Permalink | Reply | 0 comments |
headers
Zino Benaissa | 6 Mar 2000 19:52
Picon

MetaML release Version 1.0

The Pacific Software Research Center at the Oregon Graduate Institute
is proud to announce the first public release of MetaML. For more
information, and directions on how to download and install the system
please refer to the webpage:
  http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html

MetaML is a meta-programming system designed to make the
construction of meta-programs such as program generators safe and
easy. In a meta-programming system meta-programs manipulate
object-programs. Meta-programs may construct object-programs,
combine object-program fragments into larger object-programs,
observe the structure and other properties of object-programs, and
execute object-programs to obtain their values.

In addition to these operational properties, a meta-programming
system should also have a good human-system interface. MetaML
provides the following benefits:

1) It is easy to construct code using pattern-based object-code
templates. Templates  look like the object language they represent.

2) Program fragments are easy to combine into larger program
fragments, this is accomplished by a parameterizable splicing
mechanism analogous to a "template-with-holes".

3) Object-code has a parametric type, i.e., there is code with type
Int, code with type Float, etc. Type correctness of the
meta-program, guarantees type correctness of the object-programs it
constructs.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Sandro Etalle | 8 Mar 2000 10:56
Picon

International Summer School on Computational Logic

       F I R S T   C A L L   F O R    P A R T I C I P A T I O N
				   
			~~~~~~~~~~~~~~~~~~~~~~

	  International Summer School on Computational Logic
			      ISCL 2000
				   
		    Maratea (Italy), September 3-8
	http://www.cs.unimaas.nl/~etalle/school2000/index.html

				 AIM

The school is addressed to young researchers and PhD students, as well
as to university and industry researchers. Its main goal is to give
the participants an insight of some relevant research lines in
Computational Logic.

			      PROGRAMME

The school consists of six lectures on different topics, including
theoretical foundations and practical perspectives. Each lecture
covers one topic from basic notions to more advanced issues.  PhD
students may ask to have a proficiency final exam at the end of the
school.  The lecturers and the topics are the following:

- Moreno Falaschi (University of Udine, Italy). Optimization of
  declarative languages.

- Thom Fruehwirth (LMU Munich, Germany). Constraint Programming.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Martin Henz | 9 Mar 2000 01:55
Picon
Favicon

CP2000: Final Call for Papers [NEW SUBMISSION DATES]


[ Benjamin C. Pierce asked me to write a short prolog underlining the ]
[ relevance of CP2000 for TYPES readers. Although not being an expert ]
[ in this area, here my 10 cents.                                     ]
[                                                                     ]
[       Martin Henz                                                   ]
[       Publicity Chair, CP2000                                       ]

Constraint-based formalisms have been proved useful for several kinds
of type inference and type checking methods. Examples include the
use of constraints for simpler reformulations of classical type inference
methods such as Hindley-Milner-style polymorphic type inference, mode
analysis for concurrent logic programming, binding time analysis in logic
programming etc. The conference CP2000 invites submissions on typing that
use constraint-based or constraint-related methods.

[It is my standard policy to request such prologs for announcements of
events that are not self-evidently relevant to Types.  This turns out
to have two good effects: the posters of most announcements never
respond to my request, and the ones that do always add useful
information.  Thanks, Martin!  -- BCP]

                   Sixth International Conference on
           Principles and Practice of Constraint Programming

                   September 18-22, 2000, Singapore

                   http://www.comp.nus.edu.sg/~cp2000

                            CALL FOR PAPERS
(Continue reading)

Permalink | Reply | 0 comments |
headers
MFCS 2000 | 9 Mar 2000 13:19
Picon
Favicon

MFCS 2000 - Submission Deadline Approaching

      Please note that the submission deadline is MARCH 24, 2000.

**************************************************************************
                                 MFCS 2000

                      25th International Symposium on
              Mathematical Foundations of Computer Science 

                       August 28 - September 1, 2000 
                     Bratislava, Slovak Republic, Europe

                             http://www.mfcs.sk/

**************************************************************************
                              CALL FOR PAPERS
**************************************************************************

The series of MFCS symposia, organized alternately in the Czech Republic,
Poland and Slovakia since 1972, has a long and well-established tradition.
The MFCS symposia encourage high-quality research in all branches of
theoretical computer science. Their broad scope provides an opportunity to
bring together specialists who do not usually meet at specialized
conferences. Papers presenting original research on theoretical aspects of
computer science are solicited.

Principal topics of interest include (but are not limited to): design and
analysis of algorithms (sequential, parallel, distributed, approximation,
computational biology, computational geometry, graph, network, on-line,
optimisation) and data structures, algorithmic learning theory, automata,
grammars and formal languages, structural and computational complexity,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Frank Pfenning | 9 Mar 2000 15:22
Picon

Postdoctoral Research Associate


		    POSTDOCTORAL RESEARCH ASSOCIATE

		     Department of Computer Science
		       Carnegie Mellon University

The Fox project on Advanced Language Technology for Extensible Systems
under the direction of Robert Harper, Peter Lee, and Frank Pfenning is
looking for a postdoctoral researcher.  Applicants should have
background and interests in one or more of the following areas:

  - design and implementation of ML and related languages
  - advanced type systems, proof-carrying code and certifying compilation
  - embedded systems, network software and safety infrastructure

The ideal candidate will have credentials in system building and a
lively interest in language theory.  Participation in teaching
activities is also encouraged.  The appointment is initially for one
year with a potential renewal for a second year.  Salary is negotiable
and commensurate with experience.

The Fox project is working to demonstrate the viability and benefits of
advanced languages for programming real-world systems, with an emphasis
on networking, mobile code, and related safety and efficiency problems.
For more information on the Fox project, see http://foxnet.cs.cmu.edu/.

Please direct inquiries and applications to

  Frank Pfenning
  Department of Computer Science
(Continue reading)

Permalink | Reply | 0 comments |

Gmane