delia Kesner | 2 Oct 1998 11:38
Picon

workshop announcement


                         W E S T A P P'  9 9

       The Second International Workshop on Explicit Substitutions: 
             Theory and Applications to Programs and Proofs

                        CALL FOR PAPERS
                    July 5, 1999, Trento, Italy
                    FLoC'99 Affiliated Workshop 

         URL address: http://www.lri.fr/~kesner/westapp/call.html

Recently,  there has been growing  interest  in explicit substitutions as a
means of bridging the gap between theory and practice in the implementation
of   programming      languages,       theorem   provers      and     proof
checkers. Theoretically,    these  typically rely  on  calculi  that employ
substitution operations implicitly  at the meta-level; implementations  are
then   framed   in   terms  of  these     meta-level  operations.  Explicit
substitutions bring  the meta-level operations  down  into the object-level
calculus, where  they are represented  explicitly.  This  allows formal and
robust  models    to be   given  for  the   techniques  actually    used in
implementations, and  at the same time  allows more flexibility and control
on  unfinished  evaluations.  Explicit substitutions,   and more  generally
environment  machines, have recently proved to   be very useful in building
more efficient  programming languages and  proof assistants.  

The aim of this  workshop is to bring  together researchers working on both
theoretical and applied   aspects  of explicit substitutions,  to   present
recent work  (possibly  still in progress), and   to discuss new  ideas and
emerging trends in topics including the following: 
(Continue reading)

Kwangkeun Yi | 2 Oct 1998 17:41
Picon

position opennings

          RESEARCH PROFESSORS AND FULL-TIME RESEARCH ASSOCIATES

	       ROPAS: Research On Program Analysis System
	      National Creative Research Initiative Center
 	    Korea Advanced Institute of Science & Technology

The ROPAS center is looking for 2 research professors (Ph.D.) and
research staffs of Ph.D.- or M.S.-level. Applicants should have
background and interest in one or more of the following areas:  

  - semantic-based program analyses
  - program specification and proof
  - computational logics and calculi
  - compiler systems for HOT (higher-order, typed) programming languages
  - compiler systems for conventional imperative languages
  - programming language semantics
  - programming environment and tools
  - functional programming
  - financial or numerical software system

The center's flagship project is "The LET Project: program analysis for
generating smalL, safE, and smarT code," which focuses on HOT language
compilers for generating codes that are as small as possible, can be
checked against safety violation, and are self-optimizing.
The center's research staffs will cooperate on  compiler systems,
programming language theories, and semantics-based static analysis. 

- The appointment is initially for one to three years with a potential renewal
  for the next three years.
- Salary is competitive, negotiable, and commensurate with experience.
(Continue reading)

John Harrison | 6 Oct 1998 20:22
Picon
Picon
Favicon

Book: "Theorem Proving with the Real Numbers"

[While not connected with the contemporary lines of research in type theory,
 the following book discusses the formalization of some non-trivial classical
 mathematics in simple type theory. It will be of particular relevance to
 those interested in mechanized theorem proving, and in how informal
 mathematics fits into formal systems.]

People interested in the formalization of mathematics, computer-aided
verification and related fields may like to know that a revised version
of my PhD thesis is now available from Springer-Verlag. The following
information is taken from the publisher's Web page

  http://www.springer.co.uk/comp/books/key.html

You can conveniently order the book directly from that page.

    Theorem Proving with the Real Numbers

    John Harrison

    Theorem Proving with the Real Numbers discusses the formal development
    of classical mathematics using a computer. It combines traditional
    lines of research in theorem proving and computer algebra and shows
    the usefulness of real numbers in verification. This book aims to show
    that a theory of real numbers is useful in practice as well as
    theoretically interesting, and that the 'LCF' style of theorem proving
    is well suited to the kind of work described.

    CONTENTS: Introduction - Constructing the Real Numbers - Formalized
    Analysis - Explicit Calculations - A Decision Procedure for Real
    Algebra - Computer Algebra Systems - Floating Point Verification -
(Continue reading)

Tobias.Nipkow | 12 Oct 1998 16:31
Picon
Favicon

A new proof of the wellfoundednes of the multiset ordering

Dear colleagues,

Attached you find a new(?) proof of the wellfoundednes of the multiset
ordering due to Wilfried Buchholz. Salient features:
- it is completely inductive and does not involve classical reasoning (in
contrast to the proof by Dershowitz and Manna);
- it is a joy for theorem provers (it takes about 40 lines in Isabelle/HOL).

I would be interested to hear if this proof is known in the literature.

Tobias

%!PS-Adobe-2.0
%%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software
%%Title: multiset.dvi
%%Pages: 2
%%PageOrder: Ascend
%%BoundingBox: 0 0 596 842
%%DocumentPaperSizes: a4
%%EndComments
%DVIPSCommandLine: dvips multiset.dvi -o multiset.ps
%DVIPSParameters: dpi=600, compressed, comments removed
%DVIPSSource:  TeX output 1998.10.12:1306
%%BeginProcSet: texc.pro
/TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N
/X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72
mul N /landplus90{false}def / <at> rigin{isls{[0 landplus90{1 -1}{-1 1}
ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale
isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div
hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul
(Continue reading)

chet | 12 Oct 1998 20:36
Picon
Favicon

Re: A new proof of the wellfoundednes of the multiset ordering


Didn't Steve Simpson do a bunch of proofs of orderings like this one?
And I thought that even he referenced Diana Schmidt (though perhaps I
have the name wrong) from Heidelberg?

--chet--

    TN> Attached you find a new(?) proof of the wellfoundednes of the
    TN> multiset ordering due to Wilfried Buchholz. Salient features:
    TN> - it is completely inductive and does not involve classical
    TN> reasoning (in contrast to the proof by Dershowitz and Manna);
    TN> - it is a joy for theorem provers (it takes about 40 lines in
    TN> Isabelle/HOL).

    TN> I would be interested to hear if this proof is known in the
    TN> literature.

Paul Bonnington | 13 Oct 1998 01:14
Picon
Picon
Favicon

DMTCS'99 and CATS'99 Call for Participation

Call for Participation:

  DMTCS'99, Discrete Mathematics and Theoretical Computer Science

			     and

      CATS'99, Computing: The Australasian Theory Symposium

      University of Auckland and CDMTCS, Auckland, New Zealand

			18-21 January 1999

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

  
DMTCS'99 and CATS'99 will be part of the Australasian Computer Science Week
(ACSW'99) which is being held in the beautiful New Zealand city of Auckland
(City of Sails, Museums, Cafes, Restaurants, Polynesian and Maori Culture
and more).  See http://www.tcs.auckland.ac.nz/~acsw99 for more information.

[ Note that a Java Teaching Day was appended to the conference for Friday 
January 22nd, immediately after the ACSW'99 conferences. ]

For the DMTCS/CATS'99 satellite conference there will be five invited papers 
plus 19 contributed papers.

Invited Speakers:

   R. Downey (U. Victoria, NZ).
   Parametric Complexity After (almost) Ten Years: Review and Open Questions
(Continue reading)

Gopalan Nadathur | 14 Oct 1998 04:16
Favicon

a repository for CS research


I include below an announcement of a newly created repository for CS
research. There are at least two subareas in this repository,
Programming Languages and Logic in Computer Science, that should be of
interest to subscribers to this mailing list. 

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

Announcing A Computing Research Repository

Researchers have made their papers available by putting them on personal
web pages, departmental pages, and on various ad hoc sites known only
to cognoscenti.  Until now, there has not been a single repository to 
which researchers from the whole field of computing can submit reports.  

This is about to change.  Through a partnership of ACM, the Los Alamos 
e-Print archive, and NCSTRL (Networked Computer Science Technical
Reference Library), an online Computing Research Repository (CoRR) is 
being established.  The Repository has been integrated into the 
collection of over 20,000 computer science research reports and other 
material available through NCSTRL (http://www.ncstrl.org) and will be 
linked with the ACM Digital Library.  Most importantly, the Repository 
will be available to all members of the community at no charge.

We encourage you to start using the Repository right away.  For more details,
see http://xxx.lanl.gov/archive/cs/intro.html.  That site provides 
information on how to submit documents, browse, search, and subscribe to 
get notification of new articles of interest.  Please spread the word 
among your colleagues and students.  CoRR will only gain in value as
more researchers use it.  
(Continue reading)

Tobias.Nipkow | 16 Oct 1998 09:22
Picon
Favicon

An old proof of the wellfoundednes of the multiset ordering

The proof that the multisets ordering preserves wellfoundedness that I posted
here on Monday had already been discovered by Thierry Coquand. He told me

> I had a similar argument in An Analysis of Ramsey Theorem, Information
> and Computation 110, 1994, p. 297-304. This is lemma 7 (at the end
> in the remarks, I point out that this can be used for proving that
> a multiset extension of a wf relation is wf).

Tobias

CL Advertisement | 20 Oct 1998 11:50
Picon

International Masters Programme in Computational Logic

International Masters Programme in COMPUTATIONAL LOGIC

The Dresden University of Technology is offering a two-year study
programme, in English, leading to a master of science in computational
logic (together with a German "Diplom in Informatik").  The programme is
sponsored by the European Network of Excellence in Computational Logic
(COMPULOG Net) and other German institutions.

Past and present teachers include:

           Oskar Bartenstein                Jim Lipton
     Maria Paola Bonacina                 Faron Moller
         Anatoli Degtyarev              Michael Posegga
          Enrico Franconi                 Horst Reichel
         Alessio Guglielmi                Joerg Siekmann
         Steffen Hoelldobler            Michael Thielscher
          Dieter Hutter                   Heiko Vogler
         Michael Kohlhase                Andrei Voronkov
         Giorgio Levi                 Christoph Weidenbach

Courses focus on logic and constraint programming, artificial
intelligence, type theory, model theory, proof theory, equational
reasoning, databases, natural language processing, planning and formal
methods, among others.

The tuition fees are waived.  At the end of the programme a research
master thesis has to be discussed.

Prerequisites are a good knowledge of the basics of logic, and
familiarity with mathematical reasoning.  Knowledge of foundations of
(Continue reading)

Agostino Cortesi | 20 Oct 1998 13:40
Picon
Favicon

Static Analysis Symposium '99 (cfp)


*************************************************************************

                         First Call For Papers

             International Static Analysis Symposium (SAS'99) 

                           Venezia, Italy, 
                        22--24 September 1999 

*************************************************************************

Static Analysis is increasingly recognised as a fundamental tool for
high performance implementations and verification systems of high-level
programming languages. The last two decades have witnessed substantial
developments in this area, ranging from theoretical frameworks to
design, implementation, and application of analysers in
optimising compilers.

The Sixth International Static Analysis Symposium (SAS'99) will be held 
in Venezia, together with LOPSTR'99, hosted by Ca' Foscari University.
Previous symposia were held in Namur, Glasgow, Aachen, Paris, and Pisa.  

The technical program for SAS'99 will consist of invited lectures, tutorials, 
panels, presentations of refereed papers, and software demonstrations. 
Contributions are welcome on all aspects of Static Analysis, including, 
but not limited to

      Abstract Interpretation            Data Flow Analysis 
      Complexity Analysis                Theoretical Frameworks  
(Continue reading)


Gmane