[TYPES/announce] LFMTP-07: Call for participation

2007-06-12 Thread Carsten Schuermann
[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

   Second International Workshop on
Logical Frameworks and Meta-Languages:
 Theory and Practice
   (LFMTP'07)

 15 July, 2007
Bremen, Germany
  http://www.cs.mcgill.ca/~bpientka/lfmtp07/

A CADE-21 affiliated workshop
   http://www.cadeconference.org/meetings/cade21/


Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science.  Their
design and implementation has been the focus of considerable research
over the last two decades, using competing and sometimes incompatible
basic principles.

This workshop will bring together designers, implementors, and
practitioners to discuss all aspects of logical frameworks.  Topics
include, but are not limited to:

- logical framework design
- meta-theoretic analysis
- applications and comparative studies
- implementation techniques
- efficient proof representation and validation
- proof-generating decision procedures and theorem provers
- proof-carrying code
- substructural frameworks
- semantic foundations
- methods for reasoning about logics
- formal digital libraries.


Invited speaker:

Randy Pollack.
  Locally Nameless Representation and Nominal Isabelle

Accepted papers:

Alberto Momigliano, Alan J. Martin and Amy P. Felty.
  Two-Level Hybrid: A System for Reasoning Using Higher-Order 
Abstract Syntax

William Lovas and Frank Pfenning.
  A Bidirectional Refinement Type System for LF

Paul Callaghan.
  Coercive Subtyping via Mappings of Reduction Behaviour

Brigitte Pientka, Florent Pompigne and Xi Li.
  Focusing the Inverse Method for LF: a Preliminary Report

Julien Narboux and Christian Urban.
  A Formalisation of the Logical Relation Proof given by Crary for
  Completeness of Equivalence Checking

Alexandre Buisse and Peter Dybjer.
  Formalizing Categorical Models of Type Theory in Type Theory

Michael Zeller, Aaron Stump and Morgan Deters.
  A Signature Compiler for the Edinburgh LF

Anders Schack-Nielsen.
  Induction on Concurrent Terms

Fredrik Lindblad.
  Higher-Order Proof Construction Based on First-Order Narrowing

Murdoch Gabbay and Stephane Lengrand.
  The Lambda Context Calculus

Registration to the LFMTP workshop is independent from registration to
CADE-21.  http://www.cadeconference.org/meetings/cade21/registration.html


I hope to see you there,

Best regards,
Carsten Schuermann





[TYPES/announce] Assistant Professor Position in IST Lisbon, Deadline 18 June

2007-06-12 Thread Ana Almeida Matos
[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


  Assistant Professor Position in IST Lisbon, Portugal

* Application deadline: 18 June 2007 *


The Department of Information Systems and Computer Engineering at the 
Technical University of Lisbon, is seeking candidates for a tenure track 
faculty position at assistant professor level.  More precisely, it is a 
5 year teaching+research position, for either a Professor Auxiliar 
(the selected candidate holds a PhD, salary +-28K euro net) or an 
Assistente (masters degree is required, salary +-15K euro net).  These 
5 years are considered probatory in order to obtain a full permanent 
position.  The candidate will be selected according to scientific 
activities and professional experience.

Applications consist of the following:

1 - A formal cover letter addressed to the President of IST, sent by 
registered mail to

Núcleo de Gestão de Pessoal do Instituto Superior Técnico
Av. Rovisco Pais
1049–001 Lisboa.

that should contain personal identification info (name, parents names, 
nationality, birth date, identification document number and emission 
date and entity, address, telephone number), degrees and professional 
position, as well as any other elements that could be considered 
relevant to your application.

2 - A complete CV.

3 - Copy of diplomas.  Candidates who have obtained their PhD degree 
outside Portugal should register their degree in a Portuguese 
University.  To meet the deadline, it is sufficient to produce a proof 
that the registration has been requested.

The ability to speak Portuguese is valued, for teaching purposes, but it 
is not mandatory.  We expect the selected candidate to learn to be able 
to teach undergraduate courses in Portuguese, within a couple of years.

For more information about the application procedure, please contact Sr. 
António Gonçalves ([EMAIL PROTECTED]).



--- ABOUT THE DEPARTMENT ---


TEACHING

The Department participates in the following degrees of IST:

- Undergraduate degrees:

 *  Information Systems and Computer Engineering - Alameda
   https://fenix.ist.utl.pt/leic-pB
 *  Information and Communication Networks Engineering
   https://fenix.ist.utl.pt/lerci-pB
 *  Electrical and Computer Engineering
   https://fenix.ist.utl.pt/leec-pB
 *  Industrial Engineering and Management
   https://fenix.ist.utl.pt/legi-pB

- Postdgraduate degrees:

 * Master in Information Systems and Computer Engineering
https://fenix.ist.utl.pt/publico/showDegreeSite.do?method=showDescriptiondegreeID=43

 * PhD Programme on Information Systems and Computer Engineering
http://berlin.inesc-id.pt/CCPGPortal/DEIC%20(EngEng)@[EMAIL PROTECTED]

 * A new PhD Programme in Information Security, held together with 
the Department of Mathematics (for more information contact Paulo Mateus 
http://sqig.math.ist.utl.pt/pmat/)


IST web page:  http://www.ist.utl.pt/en/?language=en
Department's web page: http://www.dei.ist.utl.pt/mission.html



RESEARCH

The majority of the department's faculty carries their research in the 
following laboratories:

- INESC:  http://www.inesc.pt/
- IT: http://www.it.pt/