[TYPES/announce] Call for Posters - ICLP 2006 - Deadline: March, 14

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

                       CALL FOR POSTERS

                             ICLP'06

          22nd International Conference on Logic Programming 
             Seattle, Washington, USA, 17-20 August, 2006
                   http://www.cs.uky.edu/iclp06/

         Part of Fourth Federated Logic Conference, FLoC 2006
                http://research.microsoft.com/floc06/

CONFERENCE SCOPE

Since the first conference held in Marseilles in 1982, ICLP has been
the premier international conference for presenting research in logic
programming. Contributions (papers and posters) are sought in all areas 
of logic programming including but not restricted to:

* Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning,
  Knowledge Representation.
* Implementation: Compilation, Memory Management, Virtual Machines, 
  Parallelism.
* Environments: Program Analysis, Program Transformation, Validation and 
  Verification, Debugging, Profiling.
* Language Issues: Concurrency, Objects, Coordination, Mobility, Higher 
  Order, Types, Modes, Programming Techniques.
* Alternative Paradigms: Constraint Logic Programming, Abductive Logic 

Query: Types for post-development analysis?

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

I have been a (silent) member of the types list for several years, as I 
am interested in monitoring (and hopefully using) developments in type 
theory. I certainly make use of (reasonably) strongly types 
specification and programming languages in my work, which is regularly 
involving the analysis of third party designs/code. Within this context 
it is often hard to use developments in the type-theory, as they appear 
(at least to me) to be aimed at designing solid development languages 
and frameworks.

I know that type systems are used to design languages (and frameworks) 
that have a given collection of desirable properties, whether this be 
the traditional "shape" correctness or for some other concern such as 
guaranteeing various concurrency or security properties. I also am aware 
of the link between type theories and abstract interpretation. What I 
was wondering if anyone here knows of the application of type theories 
to the post-development analysis context?

Thanks,

Anthony.

[TYPES/announce] Final Call for Talks: TYPES 2006 workshop

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

Please note that the deadline for early registration and submission of talks
is Wednesday, 15/3/2006.

Cheers,
Thorsten

			      TYPES 2006

		Main Conference of the Types Project
		   Nottingham, UK, 18-21 April 2006

		  http://www.cs.nott.ac.uk/types06/

This is the latest meeting in a series that started 1992, the previous
conference was in December 2004 in Paris.

The topic of the meeting is formal reasoning and computer programming
based on Type Theory : languages and computerised tools for reasoning,
and applications in several domains such as analysis of programming
languages, certified software, formalisation of mathematics and
mathematics education.

TYPES 2006 is colocated with TFP 2006 (Trends in Functional
Programming) and we plan to hold a joint session on Dependently Typed
Programming.

Invited Speakers are: Bart Jacobs, Simon Peyton Jones (joint with TFP)

Re: Query: Types for post-development analysis?

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

Clarification and Summary (so far)

I have already had several useful replies to this original posting 
(thanks). But, from some of these replies it is clear that it is worth 
clarifying my use of the "post-development analysis context", thus I am 
enclosing a description that I sent individually to one of the list members.

By "the post-development analysis context" I mean the analysis of an 
existing product (program), typically by a third party (such as a 
certifier) who has to satisfy themselves that the product meets certain 
criteria (such as showing the absence of bypassing a security manager or 
exception free execution).  It is assumed that such third parties have 
little control over the development process or languages used to 
implement a product.  They may even have little sight of the development 
documentation (or even the source code).  But for the purposes of my 
initial question, lets assume that both the design documentation and 
source code are available.

Having said this, another member of the list provided their own 
interpretation, which is also valid, namely, "someone has already 
written a program in a weakly-typed language but then [wants] to analyze 
that program for further properties using types? ".

Thanks for your responses, I am now in the process of following up the 
pointers you have given me. In summary, the (public*) pointers include:
 <at>  Work on index type systems (independently invented by Christopher 
Zenger and Hongwei Xi in the 90's).
 <at>  The *PURe Project (*Program Understanding and Re-engineering: Calculi 

Re: Query: Types for post-development analysis?

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

Many, if not all, of these are examples of so-called "type-based  
analysis" in which reasoning about a program is set up as a type  
system rather than as a problem in model checking, abstract  
interpretation, data flow analysis, etc.  Jens Palsberg has a page on  
this topic that contains pointers to many papers (though it appears  
somewhat dated): http://www.cs.ucla.edu/~palsberg/tba/

There is a survey paper he wrote on this topic that is quite  
accessible: http://www.cs.ucla.edu/~palsberg/tba/papers/palsberg- 
paste01.pdf

-Mike

On Mar 9, 2006, at 5:20 AM, Michael Anthony Smith wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Clarification and Summary (so far)
>
> I have already had several useful replies to this original posting
> (thanks). But, from some of these replies it is clear that it is worth
> clarifying my use of the "post-development analysis context", thus  
> I am
> enclosing a description that I sent individually to one of the list  
> members.
>
> By "the post-development analysis context" I mean the analysis of an

[TYPES/announce] Three Research Positions - Foundations of Distributed Computation

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

[Apologies for multiple posting!]

We'd be grateful if you could draw this to the attention of any
suitable candidates.  Thanks,
Peter

RESEARCH ASSOCIATE/RESEARCH ASSISTANT (THREE POSTS)
Foundations of Distributed Computation

Computer Laboratory, University of Cambridge

<http://www.cl.cam.ac.uk/users/pes20/advert2.html>

Ref No: NR60
Grade: NRAS Salary: £20,044 - £30,002 pa. 
Grade: RAST Salary: £20,044 - £22,289 pa

Limit of tenure: Up to two years for two Research Associate positions;
one year for one Research Assistant position.

Three Research Assistant/Research Associate positions are available in
the foundations of distributed computation, funded by EPSRC grants
EP/C510712 (Sewell, Gibbens, Norrish) and GR/T11715 (Sewell, Pitts).

[TYPES/announce] CFP: Internatinational Workshop on Software Verification and Validation

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

SVV'06: 4th Internatinational Workshop on Software Verification and 
Validation
                                   August 21, 2006, Seattle, USA
                             http://www.comp.nus.edu.sg/~abhik/svv06/

                                            In Conjunction with
                              Federated Logic Conferences (FLoC) 
2006          

                                     ***********************
                                    *** CALL FOR PAPERS ***
                                     ***********************

Goal of the Workshop
====================

Software is playing an important role in economy, government, and military.
Since software is often deployed in safety critical applications, 
correctness
and reliability have become issues of utmost importance. Techniques for
verification and validation traditionally fall into three main categories.
The first category involves informal methods such as software testing and
monitoring. The second involves formal verification, i.e., model 
checking and
theorem proving. The third is abstract interpretation and static program
analysis techniques.

[TYPES/announce] 4th workshop on Quantum Programming Languages

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

[The study of programming languages for quantum computing raises,
among other things, interesting type-theoretic questions. Hence I hope
that this announcement will be of interest to the types community. -PS]

			   CALL FOR PAPERS

     4th International Workshop on Quantum Programming Languages
			      (QPL2006)

		       July 17-19, 2006, Oxford

	    http://www.mathstat.dal.ca/~selinger/qpl2006/

				* * *

  The goal of this workshop is to bring together researchers working
  on mathematical foundations and programming languages for quantum
  computing. In the last few years, there has been a growing interest
  in logical tools, languages, and semantical methods for analyzing
  quantum computation. These foundational approaches complement the
  more mainstream research in quantum computation which emphasizes
  algorithms and complexity theory.

  Possible topics include the design and semantics of quantum
  programming languages, new paradigms for quantum programming,
  specification of quantum algorithms, higher-order quantum
  computation, quantum data types, reversible computation, axiomatic

Eliminators in type theory

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

I would like to understand  how powerful the eliminators of inductive types
can be in type theory.

Suppose a type system has the type of natural numbers ONLY, that is, we have
only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
computation rules.

Can we define fib function in such a system? Note that we don't have pairs
and function types.

fib 0 = 1
fib 1 = 1
fib (n+2) = fib n + fib (n+1)

In such a  system, we know some functions can be defined, for example,
plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
If we add the type of pairs, then more efficient fib can be easily defined.

Thanks,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent

Re: Eliminators in type theory

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

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> I would like to understand  how powerful the eliminators of inductive types
> can be in type theory.
> 
> Suppose a type system has the type of natural numbers ONLY, that is, we have
> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
> computation rules.

This is a functional representation of arithmetic, i.e. Goedel's system T. All functions 
provable total in arithmetic can be defined. Adding dependent types doesn't affect the 
strength of the system, nether does the addition of pairs (whether dependent or not).

T.

> 
> Can we define fib function in such a system? Note that we don't have pairs
> and function types.
> 
> fib 0 = 1
> fib 1 = 1
> fib (n+2) = fib n + fib (n+1)
> 
> In such a  system, we know some functions can be defined, for example,
> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
> If we add the type of pairs, then more efficient fib can be easily defined.