[TYPES/announce] Post-Doc position in the CerCo FET-Open EU Project

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

Job description:

We are currently looking for a Post-Doc position at the Department of
Computer Science, University of Bologna, to work on the CerCo FET-Open
EU Project (see description below). The gross salary is 36000 euros per
year. The University of Bologna is the oldest western university and the
Department of Computer Science (http://www.cs.unibo.it/en/), located in
the historic city center, has strong expertise in theoretical computer
science and logic and it participates to several national and
international projects. The Post-Doc will join the HELM team, leaded by
Prof. Asperti, whose members work in the domains of Type Theory and
Mathematical Knowledge Management. The CerCo project is headed by
Dr. Sacerdoti Coen. The candidate will benefit from exchange opportunity
with the other project participants (University Paris-Diderot, Paris,
and University of Edinburgh, Edinburgh). The candidate will not have any
teaching duties.

Requirements:

Candidates should have a Ph.D. in Computer Science and previous
experience in either Type Theory (in particular Interactive Theorem
Proving) or Compiler Development, and being proficient in functional
programming languages.

Starting date:

The starting date will be decided together with the candidate and could

Implementations using explicit substitutions

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

Dear colleagues,

We are currently writing a paper on explicit substitution calculi, and we
would like to include references to implementations of proof
assistants, theorem provers, and programming languages that use them.  

If you are aware of any such system please send us an email. 

Best regards,
-- Anders Schack-Nielsen and Carsten Schuermann

Re: Implementations using explicit substitutions

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

This is not a programming language or theorem prover per-se, but James 
Chapman's thesis, Type checking and normalisation*, uses a term representation 
with explicit substitutions for doing the titular activities in a (total,) 
dependently typed functional language. The thesis is written mainly in 
Epigram, but it could be translated into plenty of other languages.

Cheers,
-- Dan

* http://www.cs.ioc.ee/~james/PUBLICATION.html

[TYPES/announce] PhD student in the FormMath project

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

Job description
The aim of the FORMATH project(http://www.formath.cs.ru.nl) is to
develop libraries of formalized mathematics concerning algebra, linear
algebra, real number computation, and algebraic topology:
These libraries will be structured as software components, relying on
Ssreflect, which has proved its worth in the formal proof of the four
colour theorem, and to address topics that were mostly left untouched
by previous research in formal proofs or formal methods.

This work concerns formally proved algorithms for solving problems in
real arithmetics, solving problems in ordinary differential equations,
or solving problems in algebraic topology.
Our methodology is a combination of theoretical research and
technological development. The main tools will be provided by the
Mathematical Components project, for instance the Ssreflect library
for Coq proof assistants.

The four partners in the EU ForMath project are:
- Goteborg;
- INRIA;
- Nijmegen;
- La Roja.

More specifically, as a PhD student at the Nijmegen location you will
work on Work package 4;
- Real number computation and basic numerical analysis;
- The use of exact real number computation to prove inequalities.

Re: Implementations using explicit substitutions

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

Carsten Schuermann wrote:
> We are currently writing a paper on explicit substitution calculi, and we
> would like to include references to implementations of proof
> assistants, theorem provers, and programming languages that use them.  

> If you are aware of any such system please send us an email. 

Bruno Barras implemented an explicit substitution mechanism for the HOL4 
kernel.  This, and its advantages, are described in

 <at> InProceedings{Barras:2000:HOL-EVAL,
  author =       {Bruno Barras},
  title =        {Programming and Computing in {HOL}},
  crossref =  {tphols2000},
  pages =     {17--37},
  year =      2000,
  doi = {10.1007/3-540-44659-1_2},
}

Bruno's code is still part of the system.

Michael.

Re: Implementations using explicit substitutions

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

This is perhaps a non-standard application of explicit substitutions:  
in the following paper we show how to formalize and enforce a data- 
flow security property using explicit substitutions to track taints in  
the underlying language.
(The language is intended to provide an abstract model of a particular  
operating system's security environment.)

http://portal.acm.org/citation.cfm?doid=1513443.1513447

-Avik.

On Jan 6, 2010, at 8:13 AM, Carsten Schuermann wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> Dear colleagues,
>
> We are currently writing a paper on explicit substitution calculi,  
> and we
> would like to include references to implementations of proof
> assistants, theorem provers, and programming languages that use them.
>
> If you are aware of any such system please send us an email.
>
> Best regards,
> -- Anders Schack-Nielsen and Carsten Schuermann
>

Re: Implementations using explicit substitutions

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

Back in the mists of time (when the design of OO languages with generics 
were the new new thing) I ran a course on design of OO languages.  The 
interpreter used explicit substitutions as the model of variable 
binding, which provides a nice bridge between the formal model of 
substitution and an interpreter based on dictionaries.

The course description, including the sources (you'd be after 
hobbes.transform.Substitution) is at:

    http://fpl.cs.depaul.edu/ajeffrey/se580/

or you can just run the applet (yes, an applet, did I mention the class 
was a while back?) at:

    http://fpl.cs.depaul.edu/ajeffrey/se580/applet/

which shows explicit substitutions in action.

Alan Jeffrey.

Carsten Schuermann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> 
> ------------------------------------------------------------------------
> 
> Dear colleagues,

Grand Challenge Problems?

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

Colleagues

Now that the lek (er, POPL community)   has decided on vexing questions
about papers at POPL, I thought it best to consult this group on a harder
problem.  In my current job at a funding agency I am confronted by the
question, from Physicists and Control Theoreticians, "What are the main
*scientific* grand challenge problems in Programming Languages and
Systems?"   I have not too successful to date; hence this e-mail.

If y'all can come up with a list of five to ten challenges I would
appreciate it very much.  I don't take this question lightly; I had a long
chat with Jens Palsberg over the summer and I don't think we were able to
make much headway.

Sincerely
Purush Iyer

Re: Grand Challenge Problems?

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

Dear Purush Iyer, 

what is a "grand challenge"? I naturally know the funding agency 
answer: 

 a tool for extracting a huge amount of money from politicians 
 who need something graphic to convince voters that their spending
 is acceptable and produces 'good' things

but I'd like to know whether there's a "scientific" definition 
that would make it worthwhile discussing the idea on a science
mailing list. 

Thanks -- Matthias

On Jan 16, 2010, at 5:04 PM, Purush Iyer wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Colleagues
> 
> Now that the lek (er, POPL community)   has decided on vexing questions
> about papers at POPL, I thought it best to consult this group on a harder
> problem.  In my current job at a funding agency I am confronted by the
> question, from Physicists and Control Theoreticians, "What are the main
> *scientific* grand challenge problems in Programming Languages and
> Systems?"   I have not too successful to date; hence this e-mail.
> 

Two-tier reviewing process

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

By popular request, the following is a more detailed description of the
reviewing process that Dave Evans and I used for IEEE Security and 
Privacy 2009.

The reviewing process used by Oakland 2009 was adapted from a two-tier
processed used successfully by a few conferences in previous years. It was
pioneered by Tom Anderson for SIGCOMM 2006, and used subsequently
by SOSP 2007 and OSDI 2008.

Unlike most conference review processes, we had a two-tier PC, and
three rounds of reviewing. I believe that this structure helped us
make more informed decisions, led to better discussions at the PC
meeting, gave authors more feedback, and resulted in a better product
overall. We had 77 days to review 253 submissions. This may sound like
a lot of time, but reviewing for Oakland stretches across Christmas
and other winter holidays.

The PC of 50 people was divided 25/25 into 'heavy' and 'light' groups.
Despite the names, these PC members did similar amounts of work.  The
heavy members did a few more reviews and attended the PC meeting;
the light members participated in electronic discussion before the
meeting. Dividing the PC into half meant that we had a smaller group
at the PC meeting; and had more effective discussions than in previous
years. A two-tier PC also helped us recruit some PC members who
preferred not to travel. We did not distinguish between heavy and
light members in any external documents such as the proceedings. I
think this helped us recruit light members.