Andrea Asperti | 5 Feb 15:20 2008
Picon

[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
graduate and undergraduate teaching activities in computer science.
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
directed to the same address.

-- andrea asperti
(Continue reading)

Santiago Escobar | 18 Feb 18:30 2008
Picon

[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
Acceptance Notification  May   12, 2008
Camera Ready             May   26, 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
(Continue reading)

Robert Harper | 18 Feb 18:19 2008
Picon

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
(Continue reading)

Felice Cardone | 19 Feb 13:18 2008
Picon

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
and published by Elsevier (http://www.johnwoods.ca/HHL/).

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

Daniel Yokomizo | 23 Feb 06:02 2008
Picon

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.

Daniel Yokomizo | 25 Feb 02:55 2008
Picon

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
(Continue reading)

David Teller | 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. 

Michael Hauspie | 25 Feb 10:10 2008
Picon

[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
2008. The advent of nano-technology and advances in communications has made it
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
(Continue reading)

Carl Eastlund | 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
other semantics and calculi, in case that helps broaden your search.
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
(Continue reading)


Gmane