headers
Petersen, Leaf | 4 Jul 2007 03:33
Picon
Favicon

CFP: DAMP 2008

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

                        DAMP 2008: Workshop on
             Declarative Aspects of Multicore Programming
                        San Francisco, CA, USA
                      (colocated with POPL 2008)

Parallelism is going mainstream. Many chip manufactures are turning to
multicore processor designs rather than scalar-oriented frequency
increases as a way to get performance in their desktop, enterprise,
and mobile processors. This endeavor is not likely to succeed long
term if mainstream applications cannot be parallelized to take
advantage of tens and eventually hundreds of hardware threads.
Multicore architectures will differ in significant ways from their
multisocket predecessors. For example, the communication to compute
bandwidth ratio is likely to be higher, which will positively impact
performance. More generally, multicore architectures introduce several
new dimensions of variability in both performance guarantees and
architectural contracts, such as the memory model, that may not
stabilize for several generations of product.

Programs written in functional or logic programming languages, or even
in other languages with a controlled use of side effects, can greatly
simplify parallel programming. Such declarative programming allows for
a deterministic semantics even when the underlying implementation
might be highly non-deterministic. In addition to simplifying
programming this can simplify debugging and analyzing correctness.

DAMP is a one-day workshop seeking to explore ideas in programming
language design that will greatly simplify programming for multicore
(Continue reading)

Permalink | Reply | 0 comments |
headers
Atsushi Ohori | 4 Jul 2007 10:09
Picon

a paper available on "Record Unboxing", a new type-based optimization

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

Dear Colleagues,

Some of the types-list readers may be interested in the following
paper, which shows a new type-based optimization method that "unboxes"
tuples/records by flattening component tuples and changing top-level
tuples to multiple value passing. The required type based analysis is
simple but the resulting method shown to be quite effective.

This is implemented in the SML# (an extension of the Standard
ML) compiler version 0.30, which is available from:
http://www.pllab.riec.tohoku.ac.jp/smlsharp/

Any comments are welcome.

Best regards,
Atsushi

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

			Record Unboxing
               Huu-Duc Nguyen  and  Atsushi Ohori
                    RIEC, Tohoku University

http://www.pllab.riec.tohoku.ac.jp/~ohori/research/RecordUnboxing.pdf

In the conventional implementation of functional languages, tuples
(records) are uniformly implemented as heap allocated objects even
when they are used only for multiple parameter passing.  This paper
(Continue reading)

Permalink | Reply | 0 comments |
headers
Peter O'Hearn | 7 Jul 2007 10:38
Picon
Favicon

[TYPES/announce] Postdoc: Program Analysis with Separation Logic

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

Postdoc Position in Program Analysis with Separation Logic
Dept of Computer Science, Queen Mary, University of London

A full time Research Assistant position is available for 22 months  
from 1 October 2007 on the EPSRC-funded Smallfoot project. The aim of  
the project is to develop an automatic verification tool for pointer  
usage in C programs using separation logic. The project builds on an  
earlier Smallfoot prototype, and also the Space Invader program  
analysis. You should have experience in program analysis, as  
evidenced by your publication record, and relevant knowledge of  
separation logic and shape analysis. The project calls for both  
theoretical development of new ideas in program analysis and  
verification, and practical development of the tool.

Smallfoot is a jointly-funded project between Peter O'Hearn at Queen  
Mary and Cristiano Calcagno and Philippa Gardner at Imperial College.  
The advertised position is at Queen Mary, where the team also  
includes Dino Distefano and Hongseok Yang (originators of Space  
Invader). The position has become open as a result of Distefano, the  
previous RA, obtaining a 5-year research fellowship from the UK Royal  
Academy of Engineering. James Brotherston is the project's RA at  
Imperial.

The London teams maintain a close working relationship with Josh  
Berdine and Byron Cook from Microsoft Cambridge. Early work on the  
project has resulted in verification of data structure usage for  
several routines from a firewire device driver for Windows, as well
(Continue reading)

Permalink | Reply | 0 comments |
headers
Param Jyothi Reddy | 10 Jul 2007 20:26
Picon

Proof term for proof by exhaustion

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

Hi,
Lets define vector in usual way with constructors:
nil : Vector T 0
cons : Vector T n -> T -> Vector T (S n)

along with its inductive elimination rule. Let BD be type of Binary
Digits (enumeration with elements 0 and 1).

Also lets say i have proofs of some predicate P for all elements of
Vector's over BD of length 2, i.e.

p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons
(cons nil d) b.

using these How will the proof term for

(forall v : Vector BD (S S 0) ). P(v) look like?

I can use or elimination if i could build proof for:

(forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v ==
11. However i am not sure how the proof term for this looks either.

Can someone help me understand this?

Thanks,
Param
(Continue reading)

Permalink | Reply | 0 comments |
headers
Param Jyothi Reddy | 11 Jul 2007 00:55
Picon

Re: [Coq-Club] Proof term for proof by exhaustion

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

Hi Benjamin,
I wanted to look at how the actual proof term (in terms of raw CIC/PTS
type system) looks like rather than using tactics. More from
perspective of understanding type system.

The essential point is how can we express the fact that vector of
length 2 are just 00,01,10 and 11 (nothing more/nothing less)?

Param

On 7/10/07, Benjamin Werner <benjamin.werner@...> wrote:
> You need to generalize your statement, so that it makes sense for
> vectors of any length.
>
> For instance:
>
> Parameter P : (Vector bool 2) -> Prop.
>
> Definition PP (n : nat) : Vector bool n -> Prop :=
> match n as n return  Vector bool  n -> Prop with
> | (S (S O)) => fun p => (P p)
> | _              => fun _ => True
> end.
>
> Goal forall n p, PP n p.
> intros n p; case p; simpl; trivial;
>  clear n p; intros n v [|]; case v; trivial;
>  clear n v; intros n v [|]; case v; trivial.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Luís Caires | 11 Jul 2007 13:38
Picon
Favicon

[TYPES/announce] CONCUR 07: Call For Participation

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

                CALL FOR PARTICIPATION
                      CONCUR'07
18th International Conference on Concurrency Theory                    
              September 3th - 8th, 2007
                   Lisbon, Portugal

     !!! Early registration open until July 31st. !!!

CONCUR 2007, the 18th International Conference on Concurrency Theory,
will take place in the Gulbenkian Foundation, Lisbon, Portugal,
September 4 - 7, 2007. The purpose of the CONCUR conferences is to
bring together researchers working on the theory of concurrency and
its applications. Check the web site for all details about the
scientific program, social program, and registration instructions.

                 http://concur07.di.fc.ul.pt/

INVITED LECTURES
================

* Luca Aceto, Reykjavik University, Iceland

* Peter O'Hearn, University of London, UK

(Continue reading)

Permalink | Reply | 0 comments |
headers
Malcolm Tyrrell | 17 Jul 2007 16:25
Picon
Picon
Favicon

Completeness of powersimulation

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

Hi there.

I'm not sure that this is the appropriate forum for my question, so I 
apologise if it seems off-topic. If you can think of a more suitable 
forum, please tell me.

Powersimulation is a sound technique for establishing data refinement in 
theories of predicate transformers.

There is a completeness result for powersimulation (originally in [1] 
and reworked in [2]), but it is subject to a few awkward conditions. In 
particular, abstract data types may not use unbounded nondeterminacy.

Can anyone tell me if it is known whether the conditions are necessary?
If not, can anyone provide an example of the incompleteness of 
powersimulation?

The language of [2] (p223) gives the impression that the conditions are 
necessary. However, this is not clearly stated.

References:
[1] "A Single Complete Rule for Data Refinement", Paul H. B. Gardiner 
and Carroll Morgan, Formal Asp. Comput. 1993

[2] "Data Refinement: Model-Oriented Proof Methods and Their 
Comparison", W. de Roever and Kai Engelhardt, Cambridge University 
Press, 1999
(Continue reading)

Permalink | Reply | 0 comments |
headers
Param Jyothi Reddy | 30 Jul 2007 07:30
Picon

Inconsistency and non dependent sum elimination

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

Hi,
This is in the context for impredicative Prop and predicative type
hierarchy. The base type system is PTS. I was reading that in presence of
dependent elimination for sum type, elimination from Prop sort to Type sort
can lead to inconsistency in logic. Would it also hold true if we allow only
non-dependent elimination i.e. eliminating Prop into Type without depedency.

SumDependentCase Rule: (inconsistent)
     C[z] : Type   c1[x] : C[Inj_1(x)]   c2[y] : C[Inj_2(y)]   k : A+B
A + B : Prop

----------------------------------------------------------------------------------------------------------------
[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1[x], [y:B]c2[y], [z:A+B]C[z]) : C[k]

SumDependentCase Rule: (consistent??)
     C : Type   c1 : C   c2 : C   k : A+B      A + B : Prop

-----------------------------------------------------------------------------
[G, x:A, y:B, z:A+B]
     +~(k, [x:A]c1, [y:B]c2, z:A+B) : C

Would same be true for dependent Sum (Sigma) type? (instead of using direct
second projection, using a case similar to the one given for Sum case).

Thanks in advance,
Param
(Continue reading)

Permalink | Reply | 0 comments |

Gmane