headers
Nguyen Manh Tho | 6 Nov 2006 17:01
Picon

[TYPES/announce] ARES 2007 - Call for papers and workshops papers - Submission Deadline approaches in 2 weeks: 19-11-2006

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

Apologies for multiple copies due to cross postings. Please send to interested colleagues and students.

                          Call for Papers
+--------------------------------------------------------------------------------------------------------+
 The Second International Conference on Availability, Reliability and Security (AReS)
       ARES 2007 - "The International Security and Dependability Conference"

                    April 10th – April 13th,2007          
             Vienna University of Technology, Austria

                      http://www.ares-conf.org
                    http://www.ares-conference.eu
+-------------------------------------------------------------------------------------------------------+


Conference
----------------
The 1st International Conference on Availability, Reliability and Security conference (ARES 2006)
has been successfully organized in Vienna, AUSTRIA from April 20 to April 22, 2006 by the Technical
University of Vienna in cooperation with the European Network and Security Agency (ENISA). We have
attracted 250 participants for this conference with its 3 keynotes speakers and its 9 workshops held
in conjunction with.

In continuation of the successful 1st ARES conference, The Second (Continue reading)

Permalink | Reply | 0 comments |
headers
Rob van Glabbeek | 11 Nov 2006 03:44
Picon

[TYPES/announce] CfP: Special issue I&C on SOS

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

                           Call for Papers:

                            Special Issue
                                  of
                      Information & Computation
                                  on
                   Structural Operational Semantics

Aim: Structural operational semantics (SOS) provides a framework
for giving operational semantics to programming and specification
languages. A growing number of programming languages from
commercial and academic spheres have been given usable semantic
descriptions by means of structural operational semantics. Because
of its intuitive appeal and flexibility, structural operational
semantics has found considerable application in the study of the
semantics of concurrent processes. Moreover, it is becoming a
viable alternative to denotational semantics in the static analysis
of programs, and in proving compiler correctness.

Recently, structural operational semantics has been successfully
applied as a formal tool to establish results that hold for classes
of process description languages. This has allowed for the
generalisation of well-known results in the field of process
algebra, and for the development of a meta-theory for process
calculi based on the realization that many of the results in this
field only depend upon general semantic properties of language
constructs.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Nguyen Manh Tho | 13 Nov 2006 09:09
Picon

[TYPES/announce] ARES 2007 - Submission Deadline Extension: 30-11-2006 (firm deadline)

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

Due to numerous requests, the submission deadline of ARES 2007 conference was extended to Nov. 30. 
It is a firm deadline and could not be extended anymore.

Apologies for multiple copies due to cross postings. Please send to interested colleagues and students.

                                       Call for Papers
+--------------------------------------------------------------------------------------------------------+
 The Second International Conference on Availability, Reliability and Security (AReS)
       ARES 2007 - "The International Security and Dependability Conference"
                    April 10th – April 13th,2007           
             Vienna University of Technology, Austria
                      http://www.ares-conf.org
                    http://www.ares-conference.eu
+-------------------------------------------------------------------------------------------------------+

Conference
----------------
The 1st International Conference on Availability, Reliability and Security conference (ARES 2006) 
has been successfully organized in Vienna, AUSTRIA from April 20 to April 22, 2006 by the Technical 
University of Vienna in cooperation with the European Network and Security Agency (ENISA). We have 
attracted 250 participants for this conference with its 3 keynotes speakers and its 9 workshops held 
in conjunction with.

In continuation of the successful 1st ARES conference, The Second International Conference on
Availability, 
Reliability and Security (“ARES 2007 – The International Security and Dependability
Conference”)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Erik Ernst | 13 Nov 2006 23:49
Picon
Picon
Favicon

[TYPES/announce] ECOOP 2007 - CFC - 1 month

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

[Apologies for multiple copies]

  *** ECOOP 2007 ***

The 21st European Conference on Object-Oriented Programming, ECOOP 
2007, http://2007.ecoop.org/, will be in Berlin, Germany, on July 30 
to August 3, 2007.  Several submission deadlines are in approximately 
one month.

Submission dates (firm deadlines):
  - Technical papers: December 13, 2006
  - Workshop proposals: December 20, 2006
  - Tutorial proposals: December 20, 2006

The ECOOP 2007 conference invites high quality technical papers 
presenting research results or experience in all areas relevant to 
object technology, including work that takes inspiration from or 
builds connections to areas not commonly considered object-oriented.  
For more details, please visit http://2007.ecoop.org/mainconf/.

ECOOP 2007 invites proposals for workshops addressing different areas 
of object-oriented technology.  Workshops should serve as a forum for 
exchanging late breaking ideas and theories in an evolutionary stage. 
For more details see http://2007.ecoop.org/workshops/.

ECOOP 2007 invites proposals for tutorials addressing different areas 
of (post) object-orientation.  The purpose of a tutorial is to give a
(Continue reading)

Permalink | Reply | 0 comments |
headers
Till Mossakowski | 16 Nov 2006 11:28

[TYPES/announce] 9 research assistant positions available

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

9 research assistant positions (most of them TVL 13,
approx. € 35,000 to € 50,000 p.a. gross) available, at

Transregional Collaborative Research Center SFB/TR 8 Spatial Cognition:
Reasoning, Action, Interaction
at the Universities of Bremen and Freiburg, Germany	

The positions are in general concerned with interdisciplinary
long-term research in Spatial Cognition.

Some of the positions may be of interest to the readers of this list,
because formal methods, logic and category theory are used.

For details, see
http://www.sfbtr8.uni-bremen.de/openpositions.html
(in particular, projects I1, I3 and I4)

--

-- 
Till Mossakowski    Office:      Phone +49-421-218-64226
DFKI Lab Bremen     Cartesium    Fax +49-421-218-9864226
Robert-Hooke-Str. 5 Enrique-Schmidt-Str. 5   till@...
D-28359 Bremen      Room 2.051   http://www.tzi.de/~till
Permalink | Reply | 0 comments |
headers
Jeremy.Gibbons | 20 Nov 2006 17:36
Picon
Picon

[TYPES/announce] UTP'07 at IFM: Unifying Theories of Programming

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

                        First call for papers

           UTP'07 at IFM: Unifying Theories of Programming

   Organised as a special session of IFM 2007, the Sixth International
   Conference on Integrated Formal Methods

   IFM 2007 will be held at St Anne's College, Oxford, UK, from the
   2nd to the 6th of July, 2007

   http://www.ifm2007.org

   This special session follows the successful First International
   Symposium on Unifying Theories of Programming, UTP'06, and aims to
   reaffirm the significance of the ongoing UTP project, to encourage
   efforts to advance it by providing a focus for the sharing of
   results by those already actively contributing, and to raise
   awareness of the benefits of unifying theoretical frameworks among
   the wider computer science and software engineering communities.

   Technical contributions are invited on the UTP themes of
   abstraction, refinement, choice, termination, feasibility,
   concurrency and communication, as well as related issues.  These
   themes include, but are not limited to, linkage of theories,
   algebraic descriptions, healthiness conditions, normal forms,
   incorporation of probabilistic programming, timed calculi, and
   object-based descriptions.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Yong Luo | 22 Nov 2006 13:28
Picon
Favicon

An efficient program for the function (mod 3) in type theories

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

Dear all,

I am looking for an efficient program of the following function in the
Martin-Lof's type theory or UTT.

Nat is the type of natural numbers with constructors zero and succ.

f :: Nat -> Nat

f (zero) = zero
f (succ(zero)) = succ(zero)
f (succ(succ(zero))) =  succ(succ(zero))
f (succ(succ(succ(x)))) = f (x)

If a type theory has pattern matching such as
http://www.cs.kent.ac.uk/people/staff/yl41/TPF.htm

then this function can be easily programmed with a very good efficiency, for
example f (100) only takes 34 reduction steps.

In the Martin-Lof's type theory or UTT, every function is defined by
eliminators of inductive data types. I would like to know whether it is
possible to have an efficient program for the function f.

Thank you,

Yong
==============================
(Continue reading)

Permalink | Reply | 3 comments |
headers
Conor McBride | 23 Nov 2006 09:42
Picon

Re: An efficient program for the function (mod 3) in type theories

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

Hi Yong

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I am looking for an efficient program of the following function in the
> Martin-Lof's type theory or UTT.
>   

As well you know, I wrote a program which will spit out the program you 
want, given (more or less) the program you've written.

> f :: Nat -> Nat
>
> f (zero) = zero
> f (succ(zero)) = succ(zero)
> f (succ(succ(zero))) =  succ(succ(zero))
> f (succ(succ(succ(x)))) = f (x)
>   

> In the Martin-Lof's type theory or UTT, every function is defined by
> eliminators of inductive data types. I would like to know whether it is
> possible to have an efficient program for the function f.
>   

Yes it is. The pattern matching equations hold computationally for the
(Continue reading)

Permalink | Reply | 2 comments |
headers
Yong Luo | 27 Nov 2006 13:55
Picon
Favicon

Re: An efficient program for the function (mod 3) in type theories

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

Hi Conor,

Thank you.

Sent: Thursday, November 23, 2006 8:42 AM
Subject: Re: [TYPES] An efficient program for the function (mod 3) in type
theories

> Hi Yong
>
> Yong Luo wrote:
> > [ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Dear all,
> >
> > I am looking for an efficient program of the following function in the
> > Martin-Lof's type theory or UTT.
> >
>
> As well you know, I wrote a program which will spit out the program you
> want, given (more or less) the program you've written.
>
> > f :: Nat -> Nat
> >
> > f (zero) = zero
> > f (succ(zero)) = succ(zero)
> > f (succ(succ(zero))) =  succ(succ(zero))
(Continue reading)

Permalink | Reply | 1 comment |
headers
Conor McBride | 27 Nov 2006 14:48
Picon

Re: An efficient program for the function (mod 3) in type theories

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

Yong Luo wrote:
> I wrote:
>
>   
>> Yes it is. The pattern matching equations hold computationally for the
>> UTT programs which the translation spits out. Given a suitable reduction
>> strategy (ie, one designed to exploit this property of the translation),
>> you get a constant factor blowup in the number of steps, ie a larger
>> number of smaller steps.
>>
>> Hope this helps
>>     
>
> There is no doult that the function "mod 3" can be defined in the UTT, for
> example, by using pairs or similar things. My question is: what is the most
> efficient program in the UTT for this function?  I would also like to know
> how many reduction steps for f(100), roughly?
>   

Are you saying that the constant factor is important? Maybe it is, and 
maybe not. One might also question whether comparing numbers of 
reduction steps makes any sense when UTT reductions are very simple and 
pattern matching requires a more complex combination of constructor 
comparison and tuple unpacking operations. As it happens, the UTT code 
is quite similar to the Augustsson-style efficient compilation of 
pattern matching.

If the constant factor is important to you, I'm sure you can calculate
(Continue reading)

Permalink | Reply | 0 comments |

Gmane