headers
Laura Kovacs | 6 Oct 2008 09:18
Picon
Picon
Favicon

1st CFP - Workshop on Invariant Generation (WING 2009), York, UK, 22-23 March, 2009

[Please post - apologies for multiple copies.]

First Call for Papers

--------------------------
W I N G 2009

2nd International Workshop on INvariant Generation
--------------------------

March 22-23, 2009, University of York, UK
Satellite Workshop of ETAPS 2009

http://mtc.epfl.ch/events/WING09/

General
-------

Program verification has a long research tradition, but so far
its impact on development of safety critical software has been
relatively limited. A key impediment has been the overhead
associated with providing and debugging auxiliary invariant
annotations. As the design and implementation of reliable
software remains an important issue, any progress in this area
will be of utmost importance for future developments in IT.

The logically deep parts of the code are characterized by
(nested) loops or recursions. For these parts, formal program
verification is an appropriate tool. One of its biggest
challenges is automated discovery of inductive assertions,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carsten Schürmann | 8 Oct 2008 14:44
Picon
Favicon

CADE-22 first call for papers


		      FIRST CALL FOR PAPERS

			     CADE-22
      22nd International Conference on Automated Deduction
	       McGill University, Montreal, Canada
			August 2-7, 2009

		Submission Deadline: 23 Feb 2009
	      http://complogic.cs.mcgill.ca/cade22/

GENERAL INFORMATION
  CADE is the major forum for the presentation of research in all
  aspects of automated deduction. The conference programme will
  include invited talks, paper presentations, system
  descriptions, workshops, tutorials, and system competitions.

SCOPE
  We invite high-quality submissions on the general topic of
  automated deduction, including foundations, applications,
  implementations and practical experiences.

  Logics of interest include, but are not limited to

    o propositional, first-order, equational, higher-order,
      classical, description, modal, temporal, many-valued,
      intuitionistic, other non-classical, meta-logics,
      logical frameworks, type theory and set theory.

  Methods of interest include, but are not limited to
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rob Arthan | 9 Oct 2008 17:14

Re: How were type variables added to higher order logic?

[Rseend: I got no response first time round]

On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote:
> Since I began using HOL88 many years ago, I have always heard that the
> logic of HOL was "higher order logic,"
> ...
 However, when reading both of these, I see that in neither case does the
> type system proposed contain type variables within the logic.  They both
> use type variables as meta-variables, e.g. when describing an infinite
> class of related axioms, but they do not express such a notion as a single
> axiom using a type variable within the logic.
>
> It appears from checking page 11 of the HOL4 LOGIC manual, that the
> inventor of this idea was Robin Milner:
>
> 1. *Type variables: *these stand for arbitrary sets in the universe. In
> Church's original
>
> formulation of simple type theory, type variables are part of the
> meta-language
>
> and are used to range over object language types. Proofs containing type
> variables
>
> were understood as proof schemes (i.e. families of proofs). To support such
>
> proof schemes *within *the HOL logic, type variables have been added to the
> object
>
> language type system.2
(Continue reading)

Permalink | Reply | 3 comments |
headers
Tom Melham | 9 Oct 2008 18:03
Picon
Picon

Re: How were type variables added to higher order logic?

Rob, Peter:

Peter Andrews' PhD thesis, supervised by Church and published by
North-Holland in 1965, describes a simple type theory called "Q" that
definitely includes object-language type variables. In fact Q also includes
object-language universal quantification over these variables.

Tom

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 2 comments |
headers
Konrad Slind | 9 Oct 2008 19:18
Picon
Favicon

Re: How were type variables added to higher order logic?

  This prompted me to go back and check Andrews'
book "An Introduction to Mathematical Logic and
Type Theory:To Truth Through Proof". In there,
he presents Q_0, which does not have object
language type variables. Variables in the meta
language are used instead. I wonder why he
decided not to use the Q from his thesis ...

Konrad.

On Oct 9, 2008, at 10:03 AM, Tom Melham wrote:

> Rob, Peter:
>
> Peter Andrews' PhD thesis, supervised by Church and published by
> North-Holland in 1965, describes a simple type theory called "Q" that
> definitely includes object-language type variables. In fact Q also  
> includes
> object-language universal quantification over these variables.
>
> Tom
>

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 0 comments |
headers
Jeremy Dawson | 10 Oct 2008 00:24
Picon
Picon

Re: How were type variables added to higher order logic?


I'm not sure if this is of interest to readers of this thread, but here 
goes:

Elements of Functional Programming, by Chris Reade (a student level 
textbook) has this to say, at pp 396-7:

(talking about type inference)

(quote)
Note that in these inferences, we used T, T-1, ..., as meta type 
variables standing for unknown types and these unknown types may involve 
ordinary type variables such as \alpha, \beta, ... and so on.  There is 
a conceptual distinction between meta variables which we use (outside 
the system) to stand for any type and type variables which are part of 
the type system and also stand for any type.  However we can 
conveniently borrow ordinary type variables for use as meta 
type-variables to simplify the development of an algorithm.
(end quote)

Ie, the last sentence seems to say that although it is a significant 
conceptual distinction, it doesn't really matter.

A related point:  Isabelle (though not HOL) has "explicitly variable" 
variables (for both types and terms), ?a and ?'a, as well as "fixed" 
variables, a and 'a. The ? variables can be substituted for, the others 
can't.  But when a theorem is proved, the non-? variables can be changed 
to ? variables.

I've never really thought about it, but if you'd asked me I would have
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rob Arthan | 5 Oct 2008 16:43

Re: How were type variables added to higher order logic?

On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote:
> Since I began using HOL88 many years ago, I have always heard that the
> logic of HOL was "higher order logic,"
> ...
 However, when reading both of these, I see that in neither case does the
> type system proposed contain type variables within the logic.  They both
> use type variables as meta-variables, e.g. when describing an infinite
> class of related axioms, but they do not express such a notion as a single
> axiom using a type variable within the logic.
>
> It appears from checking page 11 of the HOL4 LOGIC manual, that the
> inventor of this idea was Robin Milner:
>
> 1. *Type variables: *these stand for arbitrary sets in the universe. In
> Church's original
>
> formulation of simple type theory, type variables are part of the
> meta-language
>
> and are used to range over object language types. Proofs containing type
> variables
>
> were understood as proof schemes (i.e. families of proofs). To support such
>
> proof schemes *within *the HOL logic, type variables have been added to the
> object
>
> language type system.2
> ...
> ________________
(Continue reading)

Permalink | Reply | 1001 comments |
headers
Carsten Schürmann | 10 Oct 2008 14:07
Picon
Favicon

CADE-22 call for workshop and tutorial proposals


     CADE 2009 - The 22nd International Conference on Automated  
Deduction
                    Montreal, Canada, August 2 - 7, 2009

                    http://complogic.cs.mcgill.ca/cade22/

                  Call for Workshop and Tutorial Proposals
             ----------------------------------------------------

CADE 2009 is the 22nd International Conference on Automated Deduction,
the premier conference on all aspects of automated deduction.  Topics
covered range from theoretical foundations to high-performance
implementations in a wide variety of logics and logical theories, with
applications in areas like verification and artificial intelligence.

Workshop and tutorial proposals for CADE 2009 are solicited.  Both
well-established workshops and newer or brand new ones are encouraged.
Similarly, proposals for workshops with a tight focus on a core
automated reasoning specialization, as well as those with a broader,
more applied focus, are very welcome.

1. Workshop Proposals

    Please provide the following information:

    + Workshop title.
    + Names and affiliations of organizers.
    + Brief description of workshop goals and/or topics.
    + Proposed workshop duration (from half a day to two days is
(Continue reading)

Permalink | Reply | 0 comments |
headers
Luca Paolini | 13 Oct 2008 19:35
Picon
Favicon

TLCA'09 - Preliminary Call for Papers


	Preliminary Call For Papers
	Ninth  International Conference on
	Typed Lambda Calculi and Applications (TLCA '09)

	
                 Brasilia, July 01-03, 2009

Part of Federated Conference on Rewriting, Deduction, and
Programming (RDP'09)

http://rdp09.cic.unb.br/

** Title and abstract due  19 December 2009 **
** Deadline for submission  6 January 2009 **

The TLCA series of conferences serves as a forum for presenting
original research results that are broadly relevant to the theory
and applications of typed calculi. The following list of topics
is non-exhaustive:

     * Proof-theory: Natural deduction and sequent calculi, cut
       elimination and normalisation, linear logic and proof nets,
       type-theoretic aspects of computational complexity
     * Semantics: Denotational semantics, game semantics,
       realisability, categorical models
     * Implementation: Abstract machines, parallel execution, optimal
       reduction, type systems for program optimisation
     * Types: Subtypes, dependent types, type inference, polymorphism,
       types in theorem proving
(Continue reading)

Permalink | Reply | 0 comments |
headers
Lee Pike | 14 Oct 2008 08:17
Favicon

FMCAD'08: Early registration ends Oct. 16th (Call for Participation)

Please note that early registration ends Oct. 16th, and the hotel  
registration deadline is Oct. 18th.

========================================================================
                        CALL FOR PARTICIPATION
========================================================================

                              FMCAD 2008
International Conference on Formal Methods in Computer-Aided Design
                        http://fmcad.org/2008

                         November 17-20, 2008
                  Embassy Suites Portland--Downtown
                           Portland, Oregon

========================================================================

Important Dates
===============
  Early Registration Deadline: October 16, 2008
  Hotel Registration Deadline: October 18, 2008

Conference Overview
===================
  FMCAD 2008 is the eighth in a series of conferences on the theory
  and application of formal methods in hardware and system design and
  verification. In 2005, the bi-annual FMCAD and sister conference
  CHARME decided to merge to form an annual conference with a unified
  community. The resulting unified FMCAD provides a leading
  international forum to researchers and practitioners in academia and
(Continue reading)

Permalink | Reply | 0 comments |

Gmane