headers
Jim Royer | 1 May 2002 21:47
Picon

Implicit Computational Complexity(ICC'02) Submission Deadline Extended


The deadline for submissions has been extended to May 14

The Implicit Complexity Workshop (ICC'02) will be held on 20-21 July
2002 in Copenhagen as part of the Federated Logic Conference
(FLOC'02).  Details on submissions and the conference can be 
found at http://www.cis.syr.edu/~royer/icc/.
Permalink | Reply | 0 comments |
headers
Kim Bruce | 2 May 2002 02:27
Picon

Re: Lambda calculus w/theory of computation

Thanks to the many (over 40) people who responded to my question about
materials for teaching theory of computation using lambda calculus,
RAM's, or imperative language models (WHILE or LOOP languages) rather
than Turing machines.  My hope was to find a book that used one or more
of these models and also covered the standard language and machine
hierarchies.

Unfortunately, it does not appear that there are many options for this. 
  The one good fit seems to be

Computability, Complexity, and Languages : Fundamentals of Theoretical
Computer Science (Computer Science and Applied Mathematics), 2nd
edition, by Martin D. Davis, Ron Sigal, Elaine J. Weyuker, 1994

My only question on this book is whether or not it would be suitable for
undergraduates (in my case, Junior CS majors).

The following book by Neil Jones also got a number of recommendations.
Unfortunately for me, it covers complexity rather than machines and
languages after the computability chapters.  Computability is done from
the point of view of WHILE programs and a functional languages, and 
looks quite attractive:

N.D. Jones,Computability and Complexity: From a Programming Perspective.
MIT Press, 1997.  ISBN 0262100649

Other books mentioned include two out-of-print texts:

Brainerd, Landweber: Theory of Computation, Wiley, 1974.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Sandeep K. Shukla | 2 May 2002 04:09
Picon

RE: Lambda calculus w/theory of computation

>From my experience, Martin Davis and Weyuker book is the best among the
books you mentioned. I had it as my Undergraduate supplementary text, and
Graduate text for theory of Computation. It is wonderfully written book,
much better than any other introduction to recursive function theory. Also,
the WHILE/LOOP language to parallelly develop the intuition of recursive
function theory is excellent. It is also quite appropriate for undergrads in
my opinion. The alternatives  are Sipser (more AUtomata and Complexity
theory, not much recursion theory), and Aho, Hopcroft, Ullman (same
problem), Gurari (same problem), Landweber (not so good) etc.

However, I did not see the book by Cutland (Recursive FUnction Theory) on
your list. I think it is Cambridge Univ Press book, and it has a model of
UNiversal Register Machine to introduce the notion of computation, and then
does a very good job about how to use WHILE/LOOP type language to express
computation on that machine, etc. I liked it a lot.
Also there is a book by Cohen which is pretty good, and that comes with a
disk containing Turing machine simulator etc.

Regards

Sandeep Shukla
http://www.ics.uci.edu/~skshukla
Permalink | Reply | 0 comments |
headers
Eelco Visser | 2 May 2002 19:38
Picon
Favicon

Master Program Software Technology at Utrecht University


[Please forward to potential students]

Starting in September 2002, Utrecht University (The Netherlands) will offer the

	Master Program Software Technology

The ST program studies all techniques that may be employed in the production of
actual software. We do so by starting from sound theoretical foundations, with
a strong focus on real applicability. It includes programming methodology,
programming formalisms (languages), programming tools, software architectures,
component based programming, specification formalisms and verification
techniques (correctness proofs, theorem proving).

The Master Program is internationally oriented: the program is open to foreign
students, and courses are taught in English. Students have the opportunity to
follow courses and do projects at foreign universities and institutes. There
are two streams in the program: a research-oriented track for students with a
desire to obtain a PhD position or a research position in a company, and an
industry-oriented track for students who are interested in jobs as software
designer in industry. The program results in a degree Master of Science in
Computer Science. The program is offered by the Center for Software Technology,
of the Institute of Information and Computing Sciences at Utrecht University.

The deadline for sending in applications for admission to the program is May
15, 2002.

For more information about the program see

	http://www.cs.uu.nl/groups/ST/Master/
(Continue reading)

Permalink | Reply | 0 comments |
headers
SAS2002 | 3 May 2002 10:07
Picon
Picon

SAS'02 -- DEADLINE EXTENSION -- MAY 10

Due to numerous requests, the submission deadline for SAS'02 has been
extended to:            **Friday MAY 10** 
----------------------------------------------------------------------
                       CALL FOR PAPERS (SAS'02)

            The 9th International Static Analysis Symposium 
                 September 17 - 20 2002, Madrid, Spain
                    http://clip.dia.fi.upm.es/SAS02

                  New submission deadline: May 10, 2002
----------------------------------------------------------------------

   Static Analysis  is increasingly  recognized as a  fundamental tool
for  high  performance  implementations  and verification  systems  of
high-level  programming  languages.  The  series  of  Static  Analysis
Symposia  has  served  as   the  primary  venue  for  presentation  of
theoretical, practical, and application advances in the area.

   The Ninth International Static  Analysis Symposium (SAS'02) will be
held  at   the  Technical   University  of  Madrid,   co-located  with
Logic-based Program Development and Transformation (LOPSTR'02) and the
APPIA-GULP-PRODE   Joint   Conference   on   Declarative   Programming
(AGP'02). Previous symposia were held in Paris, Santa Barbara, Venice,
Pisa, Paris, Aachen, Glasgow and Namur.

   The technical program for  SAS'02 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:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ralf Hinze | 3 May 2002 15:01
Picon
Favicon

CFP: JFP Special Issue on Functional Pearls

                               CALL FOR PAPERS

                      Special Issue on Functional Pearls

            http://www.informatik.uni-bonn.de/~ralf/necklace.html

                          [Deadline: 31 August 2002]

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

                                               Wer die Perle in Händen hält,
                                               fragt nicht nach der Muschel.
                                                              - Peter Benary

A special issue of the Journal of Functional Programming will be
devoted to Functional Pearls. The submission deadline is 31 August
2002.

Scope
-----

Do you have a paper that is small, rounded and enjoyable to read?
Please consider submitting it to the Special Issue on Functional
Pearls, as we intend to string a shiny necklace. If you don't have a
pearl, write one today! Papers can be on any subject connected to
functional programming. A pearl is typically around 8 pages, though
there is no strict page limit. The special issue also welcomes
tutorial or educational papers in a broad sense.

Submission details
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 6 May 2002 12:47
Picon
Favicon

Workshop on Proof Theory and Computation

First Call for Participation

WORKSHOP ON PROOF THEORY AND COMPUTATION
Dresden University of Technology - June 3-14, 2002
==================================================
<http://www.ki.inf.tu-dresden.de/~guglielm/WPT>

We will offer the following courses of five lectures each, aimed at
researchers and graduate students with some background in proof theory.
The focus of the workshop will be on proof theory and computation: we
aim at a small, informal event where people will have plenty of time to
exchange ideas.  Other talks can be accommodated based on interest.

Participation in the workshop is free of charge, but limited to a
maximum of 25 persons.  Assistance will be provided in finding an
accommodation in Dresden, at prices starting from 18 EUR/day.
Registration is requested, please send an email to
<mailto:wpt@...>, making sure you include a very
brief bio
(5-10 lines) stating your experience, interests, etc.  A selection
procedure will be adopted in case of excessive demand.

Each course will be entirely contained in one of the two weeks the
workshop will span.  A detailed schedule will be provided on the
workshop page.  This is the list of confirmed courses:

Week 1: June 3-7, 2002

    SPECIFYING AND REASONING ABOUT PROGRAMS IN PROOF SEARCH
    Dale Miller (Penn State, USA)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alex Simpson | 6 May 2002 15:37
Picon
Picon

Paper announcement


The following paper is now available over the Web.

           Computational Adequacy for Recursive Types
             in Models of Intuitionistic Set Theory

  We present a general axiomatic construction of models of FPC, 
  a recursively typed lambda-calculus with call-by-value operational
  semantics. Our method of construction is to obtain such models as 
  full subcategories of categorical models of intuitionistic set
  theory. This allows us to obtain a notion of model that encompasses
  both domain-theoretic and realizability models. We show that the 
  existence of solutions to recursive domain equations, needed for 
  the interpretation of recursive types, depends on the strength of 
  the set theory. The internal set theory of an elementary topos is
  not strong enough to guarantee their existence. However, solutions 
  to recursive domain equations do exist if models of intuitionistic
  Zermelo-Fraenkel set theory are used instead. We apply this result
  to interpret FPC, and we provide necessary and sufficient conditions 
  on a model for the interpretation to be computationally adequate, 
  i.e. for the operational and denotational notions of termination 
  to agree.

  http://www.dcs.ed.ac.uk/~als/Research/rec_adequacy.ps.gz
  http://www.dcs.ed.ac.uk/~als/Research/rec_adequacy.pdf.gz

Alex

--

-- 
Alex Simpson, LFCS, Division of Informatics, University of Edinburgh
(Continue reading)

Permalink | Reply | 0 comments |
headers
TPHOLs | 6 May 2002 22:20
Picon

Call for Papers - Participation

[ This conference may be of interest to TYPES readers; previous years'
  programs have included a number of papers with a type-theoretic
  dimension. --B ]

              CALL FOR PARTICIPATION - TPHOLs 2002

           CALL FOR PAPERS, CATEGORY B, WORK IN PROGRESS

The 2002 International Conference on Theorem Proving in Higher Order
Logics will be the fifteenth in a series that dates back to 1988. The
conference serves as a venue for the presentation of work in automated
deduction, formal specification, requirements, verification, and
related fields.

                       Hampton, Virginia, USA
              Tuesday 20 August - Friday 23 August 2002 

                   ** Registration is now open **
           http://shemesh.larc.nasa.gov/registration.html

           CALL FOR PAPERS - CATEGORY B, WORK IN PROGRESS

TOPICS

The program committee welcomes submissions reporting work in 
progress, on all aspects of theorem proving in higher order logics, 
and on related topics in theorem proving and verification.  

DEADLINES AND SUBMISSION PROCEDURE
(Continue reading)

Permalink | Reply | 0 comments |
headers
Roberto Di Cosmo | 7 May 2002 02:30
Picon

Remarks on type isomorphisms with the empty and sum type


The following paper (to be presented in LICS'02) is available on the Web  

                   Remarks on Isomorphisms in
          Typed Lambda Calculi with Empty and Sum Type

      by Vincent Balat, Roberto Di Cosmo and Marcelo Fiore

Tarski asked whether the arithmetic identities taught in high school
are complete for showing all arithmetic equations valid for the
natural numbers.  The answer to this question for the language of
arithmetic expressions using a constant for the number one and the
operations of product and exponentiation is affirmative, and the
complete equational theory also characterises isomorphism in the typed
lambda calculus, where the constant for one and the operations of
product and exponentiation respectively correspond to the unit type
and the product and arrow type constructors.

This paper studies isomorphisms in typed lambda calculi with empty and
sum types from this viewpoint.  We close an open problem by
establishing that the theory of type isomorphisms in the presence of
product, arrow, and sum types (with or without the unit type) is not
finitely axiomatisable.  Further, we observe that for type theories
with arrow, empty and sum types the correspondence between isomorphism
and arithmetic equality generally breaks down, but that it still holds
in some particular cases including that of type isomorphism with the
empty type and equality with zero.

The paper is available over the Web:
(Continue reading)

Permalink | Reply | 0 comments |

Gmane