headers
Eike Ritter | 4 Nov 1997 18:44
Picon
Picon
Favicon

CfP: ESSLLI-98 Workshop on Logical Abstract Machines


                          ESSLLI-98 Workshop on 
                        LOGICAL ABSTRACT MACHINES 
                           August 17 - 21, 1998

                       A workshop held as part of the 
        10th European Summer School in Logic, Language and Information 
                               (ESSLLI-98) 
                August 17 - 28, 1998, Saarbrueken, Germany

                        ** FIRST CALL FOR PAPERS **

ORGANISERS: Valeria de Paiva and Eike Ritter (University of Birmingham)

Web site: http://www.dcs.warwick.ac.uk/~esslli98/workshops.html

BACKGROUND:
This workshop brings together recent work on the design of abstract 
machines for functional programming languages based on logical foundations.  
Abstract machines describe implementations of functional languages on a 
level of abstraction which is high enough to make it possible to reason 
about the implementation but low enough as to allow an easy coding of the 
abstract machine.  The workshop is aimed at students and researchers with a 
basic understanding of functional programming and intuitionistic logic who 
want to work on the exciting field of programming with a solid logical 
basis.

We focus the workshop along two main themes: explicit substitutions and 
abstract machines based on Linear Logic.  Most of the more recent work on 
abstract machines is directed towards implementing and proving correct
(Continue reading)

Permalink | Reply | 0 comments |
headers
Zhaohui Luo | 9 Nov 1997 18:02
Picon
Picon

Workshop on-line proceedings


The on-line proceedings of the following workshop held at Durham, UK

		     TYPES Working Group Workshop on
	Subtyping, inheritance and modular development of proofs 

is now available at the following home page (the original home page
for the workshop):

http://www.dur.ac.uk/~dcs3apj/cs-types/

>From the same page you can also obtain the addresses of the attendees,
abstracts of the talks, and other relevant details of the workshop.

Alex Jones, Zhaohui Luo, Sergei Soloviev 
(Local organisers)
Permalink | Reply | 0 comments |
headers
Zhaohui Luo | 10 Nov 1997 12:39
Picon
Picon

Workshop on-line proceedings -- correction


The following web page for the on-line proceedings of the Durham
Workshop is now working.  There was a problem for some people to
access it, which should now be corrected.  We are sorry for those who
could not access the page.

Zhaohui Luo.

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

The on-line proceedings of the following workshop held at Durham, UK

		     TYPES Working Group Workshop on
	Subtyping, inheritance and modular development of proofs 

is now available at the following home page (the original home page
for the workshop):

http://www.dur.ac.uk/~dcs3apj/cs-types/

>From the same page you can also obtain the addresses of the attendees,
abstracts of the talks, and other relevant details of the workshop.

Alex Jones, Zhaohui Luo, Sergei Soloviev 
(Local organisers)
Permalink | Reply | 0 comments |
headers
Uffe Henrik Engberg | 11 Nov 1997 01:46
Picon
Favicon

BRICS Int. PhD School: Call for Admission and Grant Applications

[Please accept our apologies if you receive this more than once]

                                                   B R I C S
                                                   International PhD School
                                                   in Computer Science
                                                   University of Aarhus
                                                   Denmark
Call for Admission and Grant Applications

This is a call for admission and  grant applications from students to BRICS
International PhD   School in Computer  Science   at University  of Aarhus,
Denmark.  The  call  is  aimed   at students  starting  August  1998,  with
application deadline January 1st, 1998.

BRICS  International PhD School is an  integrated part  of the BRICS (Basic
Research in Computer Science) Research  Centre, and both  are funded by the
Danish National Research  Foundation. The   school admits 10-15    students
(Danish and   foreign) annually, and  it provides   a substantial number of
student grants.

The core areas of  the PhD School  are: Semantics of Computation; Logic  in
Computer   Science;  Computational   Complexity;  Design  and  Analysis  of
Algorithms; Programming Languages; Distributed Computing; Verification; and
Data Security and Cryptology.

The PhD school will  provide its students with  a  solid background in  the
theoretical  foundation   centred around   BRICS activities.     From  this
foundation, the  students may either  continue in one of  the core areas or
venture into  areas of a  more applied or  experimental  nature as possible
areas of thesis specialisation.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Roberto Amadio | 10 Nov 1997 12:24

Paper on co-inductive Types

I would like to announce the following paper on co-inductive types
which is appeared as `Rapport 245 of Laboratoire d'Informatique de
Marseille' and is available at the following address:

	http://protis.univ-mrs.fr/~amadio/biblio_my_amadio.html

Of course, comments are welcome. 

Roberto Amadio

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

	Analysis of a guard condition in type theory
		(preliminary report)

	Roberto M. Amadio and Solange Coupet-Grimal
	    Universite' de Provence, Marseille

			ABSTRACT

We present a realizability interpretation of co-inductive types based
on partial equivalence relations (per's).  We extract from the per's
interpretation sound rules to type recursive definitions.  These
recursive definitions are needed to introduce ``infinite'' and
``total'' objects of co-inductive type such as an infinite stream or a
non-terminating process.  We show that the proposed type system enjoys
the basic syntactic properties of subject reduction and strong
normalization with respect to a confluent rewriting system first
studied by Gimenez.  We also compare the proposed type system with
those studied by Coquand and Gimenez. In particular, we provide a
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin Pierce | 12 Nov 1997 23:47
Picon
Picon
Picon
Favicon

Two papers on "local type inference"

The following papers are available electronically through:

        http://www.cs.indiana.edu/hyplan/papers/lti.ps.gz
        http://www.cs.indiana.edu/hyplan/papers/lti-fsub.ps.gz

Enjoy,

        Benjamin Pierce

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

                         LOCAL TYPE INFERENCE

                          Benjamin C. Pierce
                          Indiana University

                           David N. Turner
                         An Teallach Limited

                    IU CSCI Technical Report #493

We study two partial type inference methods for a language combining
subtyping and impredicative polymorphism.  Both methods are LOCAL in
the sense that missing annotations are recovered using only
information from adjacent nodes in the syntax tree, without
long-distance constraints such as unification variables.  One method
infers type arguments in polymorphic applications using a local
constraint solver.  The other infers annotations on bound variables in
function abstractions by propagating type constraints downward from
enclosing application nodes.  We motivate our design choices by a
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin Pierce | 12 Nov 1997 23:47
Picon
Picon
Picon
Favicon

Paper on bounded quantification with a Bottom type

The following paper is available electronically via:

        http://www.cs.indiana.edu/hyplan/papers/bqb.ps.gz

Enjoy,

        Benjamin Pierce

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

                  Bounded Quantification with Bottom

                          Benjamin C. Pierce
                          Indiana University

                      CSCI Technical Report #492

While numerous extensions of Cardelli and Wegner's calculus of
polymorphism and subtyping, Kernel Fun, have been studied during the
past decade, one quite simple one has received little attention: the
addition of a minimal type Bot, dual to the familiar maximal type
Top.

We develop basic meta-theory for this extension.  Although most of the
usual properties of Kernel Fun (existence of meets and joins,
decidability of subtyping and typing, subject reduction, etc.) also
hold for the extended system, the presence of Bot introduces some
surprising intricacies.  In particular, a type variable bounded by Bot
is actually a synonym for Bot; such "bottom variables" must be treated
specially at several points.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin Pierce | 13 Nov 1997 02:28
Picon
Picon
Picon
Favicon

Three papers: correct URLs

The URLs that I gave in the two announcements earlier today were
missing a component.  They should have been:

        http://www.cs.indiana.edu/hyplan/pierce/papers/lti.ps.gz
        http://www.cs.indiana.edu/hyplan/pierce/papers/lti-fsub.ps.gz
        http://www.cs.indiana.edu/hyplan/pierce/papers/bqb.ps.gz

(Or, for a complete table of contents:

        http://www.cs.indiana.edu/hyplan/pierce/papers/index.html
)

Sorry 'bout that,

        B
Permalink | Reply | 0 comments |
headers
Josh Hodas | 13 Nov 1997 01:26

Need recommendation for "Logic for CS" text

[Please reply directly to the poster, not to Types.  Josh, could you
summarize the replies here in a few days?  --BCP]

I know this is the types list, not the logic list, but I suspect your
views on logic coincide more with mine, so it seems a better place to
ask.

I have convinced my department (CS) that we should have an
introductory "logic for CS" course required in our major and taken at
the sophomore level. I will be teaching this course for the first time
next semester and am looking for your suggestions as to a good text
for such a course.

The students in the course will, as I said, be mostly sophomores.
They will have had four or more semesters of calculus (we require 2
for entry to the school), and a semester of discrete math, so they are
relatively mathematically sophisticated. They will also have had one
or more semesters programming in Java / C++, and a semester course
that covers a broad variety of CS concepts including a bit of
functional programming, parsing, logic design, architecture/assembler,
etc.

The goal is to concentrate on logic as applied to CS: More proof theory
than the typical math department intor, alot of examples of using FOPC 
sentences to describe a problem (i.e., AI and database applications of
FOPC), mostly Gentzen-style proof systems, with some discussion of other
styles, hopefully some presentation of intuitionistic systems and their
connections to the foundations of CS. The emphasis will not be on proofs
of the major theorems. There will be both pen & paper, and programming 
assignments. My hope is to introduce at least one proof assistant or
(Continue reading)

Permalink | Reply | 0 comments |
headers
Leonid Libkin | 13 Nov 1997 00:03
Favicon

LICS'98: 2nd Call for Papers (text & LaTeX)


A postscript version of the call for papers is available via the LICS
web page at http://www.bell-labs.com/topic/conferences/lics.

                   Thirteenth Annual IEEE Symposium on 
                      LOGIC IN COMPUTER SCIENCE
              June 21 - 24, 1998, Indianapolis, Indiana

			   CALL FOR PAPERS

The LICS Symposium is an annual international forum on theoretical and
practical topics in computer science that relate to logic in a broad
sense.  The 1998 program will consist of invited and contributed talks
and two tutorials.  It will be preceded by workshops on Probabilistic
Methods in Verification and Real Number Computation, and followed by
workshops on Formal Methods & Security Protocols and Logic & 
Diagrammatical Information.

Suggested, but not exclusive, topics of interest for submissions
include: abstract data types, automated deduction, bounded arithmetic,
categorical models and logics, concurrency, constraint programming,
constructive mathematics, database theory, domain theory, finite model
theory, formal methods, hybrid systems, logics of knowledge, lambda
and combinatory calculi, linear logic, logical aspects of
computational complexity, logics in artificial intelligence, logics of
programs, logic programming, modal and temporal logics, model
checking, logical aspects of protocol security, quantum logics,
rewriting, semantics, software specification, type systems, universal
algebra, and verification.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane