5 Feb 15:20 2008

### [TYPES/announce] Position opening at the University of Bologna

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Department of Computer Science (http://www.cs.unibo.it) at the
University of Bologna invites expressions of interest from qualified
computer scientists to fill an opening at the associate-professor level.
The position will have a start date of November 1st, 2008.

We are seeking candidates with a proven research record and a clear
potential for leading and initiating new research activity preferably in
(but not limited to) concurrency theory and formal methods.  The
candidate will be expected to also contribute to the Department's
Applicants must be proficient in spoken Italian. They should already be
in possession of an associate-professor or equivalent position, or of an
Italian "idoneità".

Exceptional candidates holding a full-professor position abroad can be
considered for an equivalent position at the University of Bologna.

At the conclusion of this enquiry, the University of Bologna will issue
an official vacancy declaration and carry out the procedures for filling
a tenured position.

Expressions of interest, including a detailed CV and list of
publications, should be mailed for reception no later than 15 March,
2008 and addressed to profposition@... Any enquiry can be

-- andrea asperti


18 Feb 18:30 2008

### [TYPES/announce] Cfp: 3rd Int'l Workshop on Security and Rewriting Techniques Security (SecReT 2008)

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

********************************************************************
SecReT 2008

3rd International Workshop on
Security and Rewriting Techniques
http://www.dsic.upv.es/workshops/secret08

Sunday, June 22, 2008,
Pittsburgh, USA

Affiliated workshop of
the 21st IEEE Computer Security Foundations Symposium (CSF)
and the 23rd IEEE Symposium on Logic In Computer Science (LICS)

IMPORTANT DATES

Abstract Submission      March 31, 2008
Full Paper Submission    April  6, 2008
Workshop                 June  22, 2008

SCOPE

The aim of this workshop is to bring together rewriting researchers
and  security  experts, in order to  foster  their  interaction and
develop future collaborations in this area,  provide  a  forum  for


18 Feb 18:19 2008

### focusing on binding and computation

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

We are pleased to accounce a technical report on a new approach to
integrating higher-order abstract syntax with a functional programming
language:

Focusing on Binding and Computation
Daniel R. Licata, Noam Zeilberger, Robert Harper
PDF and companion code:
http://www.cs.cmu.edu/~drl/pubs.html

Variable binding is a prevalent feature of the syntax and proof theory
of many logical systems.  In this paper, we define a programming
language that provides intrinsic support for both representing and
computing with binding.  This language is extracted as the Curry-
Howard
interpretation of a focused sequent calculus with {\em two} kinds of
implication, of opposite polarity.  The \emph{representational arrow}
extends systems of definitional reflection with the notion of a scoped
inference rule, which permits the adequate representation of binding
via
higher-order abstract syntax.  On the other hand, the
usual \emph{computational arrow} classifies recursive functions over
such higher-order data.  Unlike many previous approaches, both binding
and computation can mix freely.  Following Zeilberger [POPL 2008], the
computational function space admits a form of open-endedness, in
that it
is represented by an abstract map from patterns to expressions.  As we
demonstrate with Coq and Agda implementations, this has the important
practical benefit that we can reuse the pattern coverage checking of


19 Feb 13:18 2008

### Paper announcement

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

Dear colleagues,

we are pleased to announce that our paper "History of Lambda-Calculus
and Combinatory logic" is available at the address

http://www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf

The paper is scheduled to appear as a chapter in Volume 5 of the
Handbook of the History of Logic, edited by Dov M. Gabbay and John Woods

Of course, we welcome any comment, suggestion and additional
information on the topics of the paper, namely the development of
lambda-calculi and combinatory logic from the prehistory (Frege,
Peano and Russell) to the end of 20th century.

Regards, J. R. Hindley and F. Cardone


23 Feb 06:02 2008

### Object-oriented calculi

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

Hi,

I'm currently defining a minimalist object-oriented calculus and
wanted to know if there were other research on this area, besides
Cardelli's and Nordhagen's work. I know some work on formalizations of
object systems but found few pointers in calculi. In particular I was
looking for work calculi that aren't extensions to other calculi (e.g.
lambda, pi) to express OO constructs, but calculi that are
fundamentally distinct and foundational (in the  sense that the
calculus defines only the strictly necessary and things like effects,
type systems are defined as extensions).
Any information will be much appreciated.

Best regards,
Daniel Yokomizo.


25 Feb 02:55 2008

### Re: Object-oriented calculi

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

On Mon, Feb 25, 2008 at 12:54 AM, Tim Chevalier
<catamorphism@...> wrote:
> On 2/22/08, Daniel Yokomizo <daniel.yokomizo@...> wrote:
>  > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> >
>  >  Hi,
>  >
>  >     I'm currently defining a minimalist object-oriented calculus and
>  >  wanted to know if there were other research on this area, besides
>  >  Cardelli's and Nordhagen's work. I know some work on formalizations of
>  >  object systems but found few pointers in calculi. In particular I was
>  >  looking for work calculi that aren't extensions to other calculi (e.g.
>  >  lambda, pi) to express OO constructs, but calculi that are
>  >  fundamentally distinct and foundational (in the  sense that the
>  >  calculus defines only the strictly necessary and things like effects,
>  >  type systems are defined as extensions).
>
>  It's so obvious that I hesitated to reply on-list, but I assume you've
>  looked at Featherweight Java, as detailed in ch. 19 of Pierce's _Types
>  and Programming Languages_ (and elsewhere). That chapter contains
>  citations to related work, too. But perhaps I'm misunderstanding your
>  question...

Hi,

Yes, I'm familiar with FWJ, but I don't consider it foundational
(as it includes a type system, so it isn't the smallest set of


25 Feb 13:39 2008

### Re: Object-oriented calculi

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

Have you looked at Abadi & Cardelli's _A calculus of objects_ ?

On Mon, 2008-02-25 at 01:55 +0000, Daniel Yokomizo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

--

--
David Teller
Security of Distributed Systems
http://www.univ-orleans.fr/lifo/Members/David.Teller
Angry researcher: French Universities need reforms, but the LRU act brings liquidations.


25 Feb 10:10 2008

### [TYPES/announce] [SANET 2008] Call for Paper - Deadline is today

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


[Please accept our apologies if you receive multiple copies of this email]
***** Submission deadline February 25, 2008 *****

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

Call for Paper: Second ACM Workshop on Sensor Actor Networks (SANET 2008)
organized and run in conjuntion with ACM MobiHoc 2008, May 26-30, 2008, Hong
Kong, China.

http://www.lifl.fr/POPS/SANET2008

We invite you to participate in the Second ACM Workshop on Sensor Actor
Networks, to be held in Hong Kong, China on May 26-30 2008.

Purpose
=======
Following the success of SANET 2007, we organize and run the Second ACM
Workshop on Sensor and Actor Networks (SANET 2008) in conjunction with MobiHoc
technologically feasible and economically viable to develop low-power devices
that integrate general-purpose computing with multi-purpose sensing and
wireless communications capabilities. It is expected that sensor networks will
have a significant impact on a wide array of applications ranging from
military, to scientific, to industrial, to health-care, to domestic, to
environmental, establishing ubiquitous wireless sensor networks that will


25 Feb 17:44 2008

### Re: Object-oriented calculi

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

Daniel,

Matthias Felleisen and I published a technical report in 2006 related
to this.  I'll paste a link to it below this paragraph.  Our OO
semantics called "sequence traces" formalizes the behavior of objects
with fields and methods, and is parameterized over the computation
that occurs inside single objects between messages.  The tech report
shows representations of Abadi and Cardelli's calculus, ClassicJava,
and a multiple dispatch language in our system.  This may not fit your
criteria of minimality, but perhaps it is of interest.  We also cite
Good luck!

You can find the tech report at:
http://www.ccs.neu.edu/home/cce/publications.html

--
Carl Eastlund

On Sat, Feb 23, 2008 at 12:02 AM, Daniel Yokomizo
<daniel.yokomizo@...> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>  Hi,
>
>     I'm currently defining a minimalist object-oriented calculus and
>  wanted to know if there were other research on this area, besides
>  Cardelli's and Nordhagen's work. I know some work on formalizations of