headers
Gilles Barthe | 1 Oct 2004 16:36
Picon
Picon
Favicon

post-doctoral positions at INRIA Sophia-Antipolis

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

INRIA Sophia-Antipolis is opening two post-doctoral positions to work
in the field of formal methods for security. The positions are in the
EVEREST team, and involve close collaboration with one or more of the
team ongoing research projects:

http://www-sop.inria.fr/everest/research.php

The duration of the positions is between 12 and 18 monthes,
depending on the circumstances of the researcher. The ideal
start date is before the end of 2004, although a later start
may be possible.  It is required that the researchers will
have completed a Ph.D. before starting.

We seek candidates with a strong background in one or several of
the following fields:

- security, especially language-based security

- program specification and verification

- type systems and program analysis

- theorem proving

To apply (or to ask for further details) please send an email to
everest_jobs@...

Your application should include a CV and email addresses of
(Continue reading)

Permalink | Reply | 0 comments |
headers
Kwangkeun Yi | 1 Oct 2004 07:44
Picon

union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Hi there,

I would like to extend our ML compiler's type system so that it allow
functions to be defined over the sum of multiple datatypes. (union types?)

E.g., 

type t1 = A of int | B of t1
type t2 = C | D of t2

(* accept-both : t1+t2 -> int *)
fun accept-both (A n) = n
  | accept-both (B x) = 0
  | accept-both C = 0
  | accept-both (D y) = 0

Could you point me to some papers that I have to check out to avoid
reinvention or to expect possible obstacles? 

Thank you, 

-Kwang

--
Kwangkeun Yi		http://ropas.snu.ac.kr/~kwang
Permalink | Reply | 8 comments |
headers
Jacques Garrigue | 4 Oct 2004 07:51
Picon
Picon

Re: union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

From: Kwangkeun Yi <kwang@...>

> I would like to extend our ML compiler's type system so that it allow
> functions to be defined over the sum of multiple datatypes. (union types?)
> 
> E.g., 
> 
> type t1 = A of int | B of t1
> type t2 = C | D of t2
> 
> (* accept-both : t1+t2 -> int *)
> fun accept-both (A n) = n
>   | accept-both (B x) = 0
>   | accept-both C = 0
>   | accept-both (D y) = 0
> 
> Could you point me to some papers that I have to check out to avoid
> reinvention or to expect possible obstacles? 

Well, polymorphic variants in Objective Caml allow you to do that.
You can find several papers about them on my publication page:
   http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/
"Programming with polymorphic variants" gives a good idea of the
feature and how to compile it, and "Simple type inference for
structural polymorphism" explains in detail how one can type them.
Seeing your above example, it seems that you have different ideas
about the typing, but the compilation technique may still be
interesting.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Neelakantan Krishnaswami | 4 Oct 2004 02:26
Picon

union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Kwangkeun Yi writes:
> 
> I would like to extend our ML compiler's type system so that it
> allow functions to be defined over the sum of multiple
> datatypes. (union types?)
> 
> Could you point me to some papers that I have to check out to avoid
> reinvention or to expect possible obstacles?

Hello,

Barry Jay's paper "The Pattern Calculus" is about exactly what you
describe.

<http://www-staff.it.uts.edu.au/~cbj/Publications/pattern_calculus.ps>

Another approach is to use row polymorphism to type extensible
sums. Ocaml has this feature, and calls it "polymorphic variants". I
think Didier Remy's paper "Records and Variants as a Natural Extension
of ML" introduced the idea.

<http://portal.acm.org/citation.cfm?doid=75277.75284>

--

-- 
Neel Krishnaswami
neelk@...
(Continue reading)

Permalink | Reply | 0 comments |
headers
Joshua Dunfield | 4 Oct 2004 07:14
Picon

Re: union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Kwangkeun Yi wrote:
> I would like to extend our ML compiler's type system so that it allow
> functions to be defined over the sum of multiple datatypes. (union types?)

Frank Pfenning and I have a couple of papers on typechecking union 
types (and intersections) that may be of interest: 

  http://gs146.sp.cs.cmu.edu:8080/joshuad/papers/union-assignment/ 
  http://gs146.sp.cs.cmu.edu:8080/joshuad/papers/tridirectional-typechecking/ 

Important earlier work on unions/intersections includes Reynolds' Forsythe 
papers and Benjamin Pierce's dissertation. 

This work is on generic union types, not only unions of algebraic
datatypes; if you only need unions of algebraic datatypes, perhaps
work on extensible datatypes (like SML's `exn') would be more useful.

Best,
-j.
Permalink | Reply | 0 comments |
headers
Kwangkeun Yi | 5 Oct 2004 23:27
Picon

Re: union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Hi Rowan,

Thanks for your information. 

Does your refinement type accept the "accept-both" function as it is?
I'm looking for, if any, simplest solution for the programmers,
where no modification (e.g. rewriting datatypes or adding annotations) is
necessary for such "accept-both" ftn to be type-checked. 
Your "f: (t1 -> t2) & (t2 -> t1)" ftn is quite nice, but I'm willing
to disallow it if the inference algorithm has to ask for a help from
the programmers. 

Best,

-Kwang

On Tue, Oct 05, 2004 at 12:22:09PM -0400, rowan@... wrote:
>
> I'd add to this discussion that your example could be slightly
> reformulated to use an intersection type:
> 
>   accept-both : (t1 -> int) & (t2 -> int)
> 
> Alternatively, you can easily replace the definitions of t1 and t2 by
> a single type.
> 
>  type t = A of int | B of t | C | D of t
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
rowan | 5 Oct 2004 18:22
Picon
Favicon

Re: union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Kwangkeun Yi writes:
 > I would like to extend our ML compiler's type system so that it allow
 > functions to be defined over the sum of multiple datatypes. (union types?)
 > 
 > E.g., 
 > 
 > type t1 = A of int | B of t1
 > type t2 = C | D of t2
 > 
 > (* accept-both : t1+t2 -> int *)
 > fun accept-both (A n) = n
 >   | accept-both (B x) = 0
 >   | accept-both C = 0
 >   | accept-both (D y) = 0
 > 
 > Could you point me to some papers that I have to check out to avoid
 > reinvention or to expect possible obstacles? 

I'd add to this discussion that your example could be slightly
reformulated to use an intersection type:

  accept-both : (t1 -> int) & (t2 -> int)

Alternatively, you can easily replace the definitions of t1 and t2 by
a single type.

 type t = A of int | B of t | C | D of t
(Continue reading)

Permalink | Reply | 1 comment |
headers
Costas Dimitracopoulos | 6 Oct 2004 08:52
Picon

LOGIC COLLOQUIUM '05

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

                      FIRST ANNOUNCEMENT

          LOGIC COLLOQUIUM '05 - ASL EUROPEAN SUMMER MEETING

                July 28 - August 3, 2005, Athens, Greece

The conference will highlight the following areas: Computability Theory,
Computer Science Logic, Model Theory, Philosophy of Logic, Proof Theory 
and Set Theory. The scientific program of the conference will consist of 
four short courses, twelve plenary lectures, four special sessions and 
presentations of contributed papers. Authors of contributed papers are 
invited to submit abstracts by April 15, 2005. Each accepted paper will 
be allocated a twenty-minute period for presentation and questions. 

SHORT COURSES
Computer Science Logic - Ph. G. Kolaitis, I.B.M. Almaden Research Center 
                         and U.C.S.C., U.S.A. 
Model Theory - I. Ben-Yaacov, U. of Wisconsin, U.S.A. 
Philosophy of Logic - Speaker to be announced 
Proof Theory and Constructivity - P. Aczel, U. of Manchester, U.K.

 
PLENARY LECTURES
J. Bergstra (U. of Amsterdam, Netherlands)
S. Goncharov (Novosibirsk State U., Russia)
D. Haskell (McMaster U., Canada) 
E. Jaligot (U. of Paris VII, France)
J. Moore (Boise State U., Idaho, U.S.A.)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Michal Moskal | 6 Oct 2004 11:24

papers about type inference with subtyping

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Hello,

I'm working on the type inference engine in Nemerle (http://nemerle.org/).
This is going to be a complete redesign. I'm willing to write a technical
paper with theoretical foundations along with the implementation.

Our type system is embedded in the .NET one (Java-like object oriented,
with parametric polymorphism, type variables can be constrained),
though enriched with the function types and possibly co/contravariance
(how this is going to be compiled is another matter).

There are a few requirements for the type inference engine. The most
important one is that I'm going to trade completeness for simplicity.
Error messages are also particularly important.

There are also some additional issues making type inference harder,
or at least different then in OO ML extensions -- static overloading,
mutability, nominal type system (no structural subtyping) and local
functions to name a few.

I'm asking for pointers to papers. I did some googling, and citeseer
traversing, read about type inference through constraint solving, local
type inference and so on. I'm just willing to make sure I did not miss
something.

I'm leaning toward some restricted form of constraint solving. The current
solution is a variant of the Cardelli's greedy algorithm from F<: --
it unifies variables once and for all. This is a problem, since given:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Kwangkeun Yi | 8 Oct 2004 04:39
Picon

Re: union types and overloading

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Hi Johan,

Thanks for your reply. 

> Note that the declaration of type Both is necessary in this system.  
> Note also that the argument to constructor B is still of type T1, even 
> when B is considered a constructor of type Both.

My plan roughly agrees with O'Haskell's design decision, except for one thing:
the Both declartion from the programmer. Quick question: for what did
you trade the no-extra-annotation? (Maybe I have to study your papers, but for
quick answers...)

All the best,

-Kwang

--

-- 
Kwangkeun Yi		http://ropas.snu.ac.kr/~kwang
Permalink | Reply | 1 comment |

Gmane