headers
Alessandro Armando | 1 Mar 2002 16:12
Picon

FroCoS 2002: 2nd Call for Participation

NEWS:

  - Payment by credit cards now allowed.
  - Deadline for early registration extended to March 15. (Due to many
    requests of payment via credit card which was not possible before.)
  - Tutorial on CHR added to the Workshop Program.

---

4th INTERNATIONAL WORKSHOP ON FRONTIERS OF COMBINING SYSTEMS (FroCoS'02)
  April 8 - 10, 2002, Santa Margherita Ligure (near Genova), Italy

  CALL FOR PARTICIPATION
  **********************

  http://www.mrg.dist.unige.it/conferences/frocos2002/

  The three previous international workshops on ``Frontiers of
  Combining Systems'' were held in Munich (1996), in Amsterdam (1998),
  and in Nancy (2000).  Like its predecessors, FroCoS'02 is intended
  to offer a common forum for research activities in the general area
  of combination and integration of systems, and on their practical
  use.

* Topics. The topics of interest are related to the general area of
  combination and integration of systems, including: combination of
  logics, combination of constraint solving techniques, of decision
  procedures, of term rewriting systems, combination of deduction and
  computer algebra systems, integration of decision procedures and
  other solving processes into constraint programming and deduction
(Continue reading)

Permalink | Reply | 0 comments |
headers
etaps02.VERIMAG | 2 Mar 2002 23:19
Picon
Picon
Favicon

ETAPS 2002: LAST DAYS OF EARLY REGISTRATION


      **********************************************************
      ***                                                    ***
      ***                    ETAPS 2002                      ***
      ***                 APRIL, 6-14, 2002                  ***
      ***                 GRENOBLE,  FRANCE                  ***
      ***                                                    ***
      **********************************************************
      ***                                                    ***
      ***                !!!! REGISTER NOW !!!!              ***
      ***                                                    ***
      ***    EARLY REGISTRATION EXTENDED UNTIL MARCH 9       ***
      ***                                                    ***
      **********************************************************

The European Joint Conferences on Theory and Practice of Software
ETAPS is a loose and open confederation of conferences and other
events that has become the primary European forum for academic and
industrial researchers working on topics relating to Software Science.

       ALL RECENT INFO and ONLINE REGISTRATION can be found at:

                     ******************************
                     * http://www-etaps.imag.fr/  *
                     ******************************

-----------------------------------------------------------------------
5 Conferences - 13 Satellite Events - 11 Tutorials - Tool Demonstrations
-----------------------------------------------------------------------
(Continue reading)

Permalink | Reply | 0 comments |
headers
Fairouz Kamareddine | 4 Mar 2002 14:05
Picon
Picon

Thirty Five years of Automath


		Thirty Five years of Automath
		Heriot-Watt University, Edinburgh
		Wednesday 10-Saturday 13 April 2002
		http://www.cee.hw.ac.uk/~fairouz/automath2002/

		PROGRAM ANNOUNCEMENT AND CALL FOR REGISTRATION
	http://www.cee.hw.ac.uk/~fairouz/automath2002/program.html
		

Deadline for cheap registration:  10 March 2002

Queries: email fairouz@...
Permalink | Reply | 0 comments |
headers
C.Reinke | 4 Mar 2002 14:40
Picon

Research Opportunity: Refactoring Functional Programs (UKC)

Job opportunity for postdoc / graduate Research Associate in
Refactoring Functional Programs at University of Kent. Please bring
to the attention of suitable candidates / forward as appropriate.

Types play a major role in this project, both during program
analyses to determine applicability and scope of refactorings, and
for refactoring at the type/type class level. 

----------------------------------------------- ad follows

Research Associate in Refactoring Functional Programs

Applications are invited for a three year Research Associate position
at the University of Kent at Canterbury, to work under the direction
of Professor Simon Thompson and Dr Claus Reinke on an EPSRC
funded project entitled "Refactoring Functional Programs".
Applications are welcomed from candidates with a doctorate or a
very good first degree; in the latter case a successful candidate will
have the opportunity of registering to study for a PhD.

Refactoring is the process of redesigning existing code without changing
its functionality. In our project we will explore refactoring for functional
programs and in particular we will construct a catalogue of functional
refactorings, and build a prototype tool in Haskell to support refactoring
of Haskell programs.

Applicants should be able to demonstrate strong experience of programming
in a functional programming language, preferably Haskell, and have good
communication skills.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean-Marie JACQUET | 4 Mar 2002 14:41
Picon
Favicon

Flocasa: 1st Call for Paper

                      1st International Workshop on
                  Foundations of Coordination Languages and
                          Software Architectures
                              (Foclasa 2002)

                   August 24, 2002, Brno, Czech Republic
           Workshop affiliated to CONCUR'2002, 20 - 23 August 2002.

                  http://www.fi.muni.cz/concur2002/Foclasa

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

SCOPE AND TOPICS

    Modern  information  systems  rely  more  and  more  on  combining
    concurrent, distributed, mobile and heterogenous components.  This
    move from  old systems, typically conceived  in isolation, induces
    the  need  for  new   languages  and  software  architectures.  In
    particular, coordination  languages have been  proposed to cleanly
    separate  computational aspects  and communication.  On  the other
    hand,  software  architects face  the  problem  of specifying  and
    reasoning  on non-functional requirements.   All these  issues are
    widely perceived as  fundamental to improve software productivity,
    enhance maintainability, advocate modularity, promote reusability,
    and  lead   to  systems  more  tractable  and   more  amenable  to
    verification and global analysis.         

    The aim of  the workshop is to bring  together researchers working
    on the foundations of component-based computing, coordination, and
    software architectures.  Topics of  interest include (but  are not
(Continue reading)

Permalink | Reply | 0 comments |
headers
CSL02 | 5 Mar 2002 01:48
Picon
Picon

Second Call For Papers: Computer Science Logic 2002 (CSL'02)

[ There is a PostScript copy of this Call at
  http://www.dcs.ed.ac.uk/csl02/CSL02-cfp1.ps
  for display on notice boards.                                         ]

Please note the two stage submission procedure: intentions to submit
(with title, authors and abstract) are required by 29 March; full
submissions are required by 7 April.

                          Call for Papers

            Annual Conference of the European Association for
                        Computer Science Logic

                               CSL'02

                 22--25 September 2002, Edinburgh, UK

Computer Science Logic (CSL) is the annual conference of the European
Association for Computer Science Logic (EACSL). The conference is
intended for computer scientists whose research activities involve
logic, as well as for logicians working on issues significant for
computer science. Suggested topics of interest include: automated
deduction and interactive theorem proving, constructive mathematics
and type theory, equational logic and term rewriting, linear logic,
logical aspects of computational complexity, finite model theory,
higher order logic, logic programming and constraints, lambda and
combinatory calculi, logical foundations of programming paradigms,
modal and temporal logics, model checking, functions of program
development (specification, extraction, transformation...),
categorical logic and topological semantics, domain theory, database
(Continue reading)

Permalink | Reply | 0 comments |
headers
Reinhard Kahle | 5 Mar 2002 20:31
Picon

Colloquium on the occasion of Helmut Schwichtenberg's 60th birthday

** Ein Bogen von der Beweistheorie zur Informatik **

Colloquium on the occasion of the 60th birthday of

  Helmut Schwichtenberg

  Saturday, April 6th, 2002

Mathematical Institute of the University of Munich

Speakers:

- Gerhard Jaeger, Berne
- Hans Leiss, Munich
- Peter Paeppinghaus, Munich
- Robert Staerk, Zurich
- Anne Troelstra, Amsterdam
- Jaco van de Pol, Amsterdam
- Stan Wainer, Leeds

The colloquium will start at 9am. In the evening there will be a
birthday dinner at the restaurant "Weisses Braeuhaus". We would like
to ask you to register for the dinner before March 25th using the
following web address:

http://www.mathematik.uni-muenchen.de/~minlog/register.html

For further information - also about accommodation and travel - please
consult:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Fairouz Kamareddine | 6 Mar 2002 12:20
Picon
Picon

Special issue on Mechanising and Automating Mathematics

Call for Papers

JOURNAL OF AUTOMATED REASONING

Special issue on Mechanising and Automating Mathematics

>From its begin, to its end, the 20th century provided fascinating
questions and important results in the foundations and automation of
mathematics. The first half of the 20th century saw the birth of
Hilbert's dream concerning the derivation of true formulae, Goedel's
incompleteness result which shattered Hilbert's dream, lambda
calculus, type theory, logical and set theoretical paradigms whose aim
was to give a solid and expressive foundation of mathematics without
suffering from the paradoxes. In the second half of the 20th century,
computers found a powerful role in the logical foundations of
mathematics, and provided complementary and indispensible tools for
reasoning about and representing mathematics. When in 1967, N.G. de
Bruijn started his programme of Automating Mathematics (Automath), he
was told his project will fail by Goedel's result. It seemed then,
that all the confusion that reigned at the begin of the 20th century
in the logical foundations of mathematics, had surfaced again in the
automation of mathematics. But since, the area of automating and
mechanising mathematics, has been fascinating and has given birth to
many useful tools, techniques, and systems.

This special issue will be devoted to the different approaches in
mechanising and automating mathematics. In particular, we are
interested in the following:

+ The (semi-) automation of mathematics using any of the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jim Huggins | 6 Mar 2002 21:06
Favicon

Re: Formal semantics for C

Forgive the long delay on replying to this message, but I only now have
had the chance to reply properly.

On 22 Dec 2001, Ken Friis Larsen wrote:

> "S.J.Thompson" <S.J.Thompson@...> writes:
> > Query about the formal semantics of C:
> > 
> > Are types readers aware of any work on formalizing the semantics
> > of the C programming language?

> Michael Norrish (Computer Lab, University of Cambridge) developed a
> formal model for C and embedded this model into the HOL theorem
> prover.  More information here:
>         http://www.cl.cam.ac.uk/users/mn200/PhD/

Some time ago, Yuri Gurevich and I did a formal semantics of C 
using the Abstract State Machine (ASM) methodology, then called
"evolving algebras".  You can find more information at:

	http://www.eecs.umich.edu/gasm/papers/calgebra.html 

--Jim Huggins (jhuggins@...)
Permalink | Reply | 0 comments |
headers
martinb | 8 Mar 2002 11:03
Picon
Favicon

Re: Formal semantics for C

> Some time ago, Yuri Gurevich and I did a formal semantics of C 
> using the Abstract State Machine (ASM) methodology, then called
> "evolving algebras".  You can find more information at:
> 
> 	http://www.eecs.umich.edu/gasm/papers/calgebra.html 

i'm a bit startled by this claim that you have done a "formal
semantics of C". how do you know? there is no full abstraction and
definability result (which i take to be a minimal prerequisites for a
usable formal semantics), not even a proof of soundness or a
definition of what it means for two evolving algebras to be equal

there is an immediate objection: of course in a sense full
abstraction, definability or soundness cannot be given in this setting
because the semantics of C has never been formally specified in the
first place. this is true, but it only means that what you have
defined is a semantics (rather than a semantics of C). in addition,
and slightly contradicting what i have said, every C compiler +
libraries implicitly *defines* a formal semantics, albeit a rather
complicated one, which may or may not approximate what one may expect
to be *the* semantics of C. you could test your semantics against a
compiler, although i don't recommend it

this lack of a hard test whether your semantics actually works
(in the sense that it equates exactly the translations of those
programs that are observably equivalent in C) is probably also the
reason why you write (on page 1)

  "it is not difficult to extend our description of C to include
  any desired library function or functions."
(Continue reading)

Permalink | Reply | 1 comment |

Gmane