GTA/PhD positions available

Dear All

Some GTA/PhD positions are available at the Department of Computer
Science, University of Leicester (see below). In particular, there are
several researchers who would be interested in supporting a strong
applicant in the area of formal methods or program verification.

***The deadline for PhD plans is 4 September*** (apologies for the late notice).

Thanks

Tom

---------- Forwarded message ----------
From: Computer Science HoD <cshod <at> mcs.le.ac.uk>
Date: 4 August 2010 17:14
Subject: Advert for circulation
To: Academic staff CS <cs_acad <at> mcs.le.ac.uk>
Cc: Neil Walkinshaw <n.walkinshaw <at> dcs.shef.ac.uk>, Nir Piterman
<nir.piterman <at> doc.ic.ac.uk>, Igor Razgon <ir2 <at> csmail.ucc.ie>, Andrzej
Murawski <Andrzej.Murawski <at> comlab.ox.ac.uk>

Graduate Teaching Assistant
Department of Computer Science
Package up to £13,590
(£9,641 maintenance grant plus Salary £3,949 per annum, and also
Home/EU fee waiver)
Please note, if you are a national of a non-EU country you will be
responsible for any monetary difference between International and
Home/EU fees

CAV 2011 Call For Papers

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Post-Doc and PhD positions - Semantics of Real-World Computer Systems

[Please bring these to the attention of any suitably qualified
candidates - thanks, Peter]

*********************************************************************

Research Associate
University of Cambridge - Faculty of Computer Science & Technology

Salary: £27,319 - £35,646 pa

Limit of tenure: Up to 2 years

We are seeking a Post-Doctoral Research Associate to join a lively
group working on the semantics of real-world computer systems, with a
focus on the relaxed-memory concurrency they exhibit.  Current
projects include work on the memory models of multiprocessors (x86,
Power, ARM) and of programming languages (C++0X/C1X, Java), verified
compilation of concurrent programming languages to multiprocessors,
the semantic theory of relaxed-memory concurrency, and the development
of tool support for semantics.

You should have a keen interest in applying rigorous semantic
techniques to real-world systems, with a strong background in one or
more of the following:

    * Programming Language Semantics
    * Automated Proof Assistants
    * Relaxed Memory Models
    * Program Verification

The position is funded by the EPRSC grant EP/H005633,
http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/H005633/1, led by
Peter Sewell (http://www.cl.cam.ac.uk/~pes20/), to whom enquiries
should be addressed.

Applications should include:

    * a Curriculum Vitae
    * a brief statement of the particular contribution you would make
        to the project
    * a completed form CHRIS6:
      http://www.admin.cam.ac.uk/offices/hr/forms/chris6/
    * the names and contact details (postal and e-mail addresses) of
        two or three referees.

Start date: as soon as possible after 4th October 2010

Complete applications should be sent by post to: Personnel-Admin,
University of Cambridge, Computer Laboratory, 15 JJ Thomson Avenue,
Cambridge CB3 0FD, United Kingdom, or by e-mail to
personnel-admin <at> cl.cam.ac.uk.

Quote Reference: NR07133, Closing Date: 4 October 2010

The University values diversity and is committed to equality of
opportunity.

*********************************************************************

PhD Studentships
University of Cambridge - Faculty of Computer Science & Technology

We are seeking two PhD students to join a lively group working on the
semantics of real-world computer systems, with a focus on the
relaxed-memory concurrency they exhibit.  Current projects include
work on the memory models of multiprocessors (x86, Power, ARM) and of
programming languages (C++0X/C1X, Java), verified compilation of
concurrent programming languages to multiprocessors, the semantic
theory of relaxed-memory concurrency, and the development of tool
support for semantics.

You should have a keen interest in applying mathematically rigorous
semantic techniques to real-world systems, ideally with experience in
one or more of the following:

    * Programming Language Semantics
    * Automated Proof Assistants
    * Relaxed Memory Models
    * Program Verification

Informal enquiries should be addressed to Peter Sewell
(http://www.cl.cam.ac.uk/~pes20/), including a Curriculum Vitae and a
brief statement of your background and interests.

The positions are funded by the EPRSC grant EP/H005633,
http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/H005633/1.

For UK/EU students this covers a stipend and fees.  For October 2011
entry, applications should ideally be received by December 1 2010
(applications for earlier start dates may also be considered).

Non-UK/EU students will require additional funding for the higher
level of fees. Exceptional non-EU candidates may be considered for
nomination to the Gates Cambridge Trust and Cambridge International
Scholarship competitions.  The application deadline (for October 2011
entry) for these is October 15 2010 for US applicants and December 1
for non-US applicants (note that applications must be complete by
these deadlines, including transcripts, references, degree
certificates, and research proposal).

More information on the formal application process is here:
http://www.cl.cam.ac.uk/admissions/phd/.

Quote Reference: NR07135.

The University values diversity and is committed to equality of
opportunity.

*********************************************************************

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Types'10 - Call for Participation

                         Call for Participation

                           Types Meeting 2010  
                      Warsaw, 13 -- 16 October 2010 
                       http://types10.mimuw.edu.pl

This is a reminder that the early registration deadline for Types'10 is

                          Monday, September 13

Note also that your talk should be submitted no later than September 20.
Do not hesitate to contact types10 <at> mimuw.edu.pl if you have any
questions. 
See you in Warsaw at Types 2010!

The Organizing Committee
types10 <at> mimuw.edu.pl 

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd

I want to define inverted sequence in HOL4

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: I want to define inverted sequence in HOL4

On 3/09/10 9:57 PM, anythingroom wrote:
> hi, everyone
>
>
> I want to define inverted sequence in HOL4. How can I define arrangement
> or full permutation in HOL4? Who can give me some hints on permutation?
>
> Thank you very much! I��m looking for your reply.

src/sort/sortTheory

contains a few theorems about permutations of lists.

Michael

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Release of HOL4 Kananaskis-6

I'm happy to announce the release of the latest version of HOL4 : Kananaskis-6.

Download it from http://hol.sourceforge.net.

Release notes follow.

Michael

--

                       Notes on HOL 4, Kananaskis-6 release

    We are pleased to announce the Kananaskis-6 release of HOL 4.

Contents

      * New features
      * Bugs fixed
      * New theories
      * New tools
      * New examples
      * Incompatibilities

New features:

      * The HolSmtLib library now supports proof reconstruction for the SMT
        solver Z3. (Several other SMT solvers continue to be supported as
        oracles.)

      * The pretty-printer now uses colours to convey extra information
        about terms and types as they are printed. For example, bound term
        variables are printed in green, and free variables are printed in
        blue. This colouring will happen on colour terminals such as Unix
        xterm (also the standard MacOS Terminal application), as well as
        inside Emacs.
        If you are using the Emacs mode, then the types of both sorts of
        variables are also available in a mouse-over tooltip. Moreover, the
        colours and printing-styles used in the Emacs mode for things like
        bound variables can be customised, using M-x customize.
        Besides this automatic colored pretty-printing depending on the
        term structure, it is now possible to define syntax highlighting in
        userprinters.

      * Many type variables can now be parsed and printed as lower-case
        Greek letters. For example, you can input ``:'a``, and will get
        back ``:α``. You can also input type variables using the Greek
        letters (except for the letter λ). Underneath, the type variable
        still has the name with the apostrophe: this is a purely
        presentational change.

      * Bounded rewrites work better (a few bugs were fixed here), and
        there is now also an easy way to specify that a rewrite should only
        occur on the left or right side of a term. For example, to apply
        the theorem th twice, and on the left-hand side on an equality, use

          SIMP_TAC bool_ss [Ntimes th 2, SimpLHS]

        To rewrite on the right-hand side:

          SIMP_TAC bool_ss [Ntimes th 2, SimpRHS]

        It is also possible to rewrite on the left or right sides of
        operators other than equality. See the Description manual for
        details.

      * If the block of universally quantified variables at the head of a
        clause in the definition of an inductive relation contains
        duplicate names, Hol_reln detects this and provides an informative
        error message.

      * There are two new “document-level” modes for using HOL’s
        LaTeX-pretty-printing technology (originally due to Ramana Kumar
        and Thomas Türk). In both, terms, types and theorems become
        straightforward to embed in LaTeX documents. For example, one might
        write something like

         The term \HOLtm{p1 /\ q2} is a typical conjunction.

        and have this turned into

         The term p₁ ∧ q₂ is a typical conjunction.

        after LaTeX has been run. The ASCII conjunction has turned into a
        nice LaTeX maths symbol, and the term has been parsed, allowing
        variables to be printed in italic font, and with trailing digits
        sub-scripted.

        See the Description manual for more detailed documentation.

      * Simplification of terms involving the EL operator (calculates the
        n^th element of a list) is better.

      * Some new syntax for various bag operations, including arithmetic
        symbols +, -, <, ≤ for the notions on bags that are just point-wise
        lifts of those operators on numbers (BAG_UNION, BAG_DIFF, PSUB_BAG,
        SUB_BAG).

      * New syntax for universal sets (in pred_setTheory). In ASCII mode,
        univ(:'a) is the universal set with elements drawn from type :'a.
        Another example: univ(:num) is the set of all natural numbers. With
        Unicode on, the first example prints as 𝕌(:α). The Unicode
        character used here (U+1D54C, a cute uppercase ‘U’) is beyond the
        BMP (Basic Multilingual Plane) and may not appear in many fonts.
        Rather than have to give up all of Unicode to get around this,
        there is an additional trace variable ("Unicode Univ printing") to
        turn off the use of this character, making the syntax use univ once
        more.

        Of course, the old syntax (UNIV:'a -> bool, or UNIV:'a set)
        continues to work.

      * A new “vim mode” for controlling a HOL session from within the vim
        editor. This mimicks most of the important features of the Emacs
        mode. See tools/vim for a README file about this feature. Thanks to
        Ramana Kumar for the implementation of this tool.

      * If syntax that involves non-ASCII characters is added using
        add_rule, set_fixity or overload_on, it is only used if the Unicode
        flag is set. If the Unicode flag is toggled off and then on again,
        the Unicode syntax will disappear and reappear appropriately.

      * The persistent simpset (srw_ss(), also used in SRW_TAC) can now
        have named simpset fragments removed from it using the function
        diminish_srw_ss.

      * bin/build uses earlier (cached) options when not explicitly
        overridden. In particular, kernel specifications (-expk, and the
        new -stdknl), and build-sequence file specifications are cached in
        tools/lastbuildoptions so that one can subsequently do just
        bin/build to build again with those same options. To override a
        -seq foo option, you can use the -fullbuild option.
        Other options (-symlink, -selftest) are not cached.

      * Users can configure their interactive sessions (setting output
        pretty-printing options with set_trace commands for example), by
        writing SML code into a .hol-config.sml file in their HOME
        directory. In fact, all of the following are acceptable names for
        the file: hol-config.sml, hol-config.ML, .hol-config,
        .hol-config.sml, and .hol-config.ML. The first of these that is
        found is used.
        (The meaning of “the user’s home directory” is clear on Unix
        systems. On Windows, the environment variables HOMEPATH and APPDATA
        are consulted to determine where to look.)
        The file, if it exists, is use-d into the interactive session, when
        it begins. A message is printed saying as much also.

Bugs fixed:

      * Type abbreviations used to be able to be applied to more type
        arguments than they were expecting. E.g.,

          type_abbrev("foo", ``:bool``)

        followed by

          ``:'a foo``

        used to work. No more!

      * Hol_reln now correctly accepts inductive definitions where type
        variables appear only in schematic variables.

      * Hol_reln now correctly accepts inductive definitions defining
        multiple (presumably multiply recursive) relations with schematic
        variables. Note that for a variable to be detected as schematic in
        this situation, it needs to be a parameter to all relations, even
        if it may not be used in all of them.

      * The syntax num$0 failed to parse. Thanks to Behzad Akbarpour for
        the report of this bug.

      * In Hol_datatype, nested recursion in record data types where the
        new type was also polymorphic failed. Thanks to Ramana Kumar for
        the report of this bug.

      * In Hol_datatype, nested recursion involving the itself type
        constructor could fail. Thanks to Ramana Kumar for the report of
        and fix for this bug.

      * The TypeNet data structure for indexing information by types could
        get confused if the “same” type was redefined (in the one
        interactive session) with different arities. Thanks to Ramana Kumar
        for the bug report that led to the isolation of this problem.

New theories:

      * A very simple theory string_numTheory demonstrating that strings
        and natural numbers are in bijection (with functions n2s and s2n
        constructively demonstrating this bijection).

      * A theory of trie-like trees that recurse under a finite map,
        fmaptreeTheory. This type can be used to represent recursive
        namespace-like environments.

New tools:

      * A new library HolQbfLib provides an interface to external
        Quantified Boolean Formulae (QBF) solvers. It can check
        certificates of invalidity generated by the QBF solver Squolem.

      * A bit-blasting conversion for operations on fixed-width words:
        BBLAST_CONV. This goes beyond the capabilities of WORD_BIT_EQ_CONV
        by expanding out additions and subtractions. This allows the new
        conversion to automatically handle small but tricky bit vector
        goals. For example:

          (x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)

        and

          !a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w

        (These aren’t provable with wordsLib.WORD_DECIDE.)
        Obviously bit-blasting is a brute force approach, so the new
        conversion should be used with care. It will only work well for
        smallish word sizes and when there is only and handful of additions
        around. It is also “eager”—additions are expanded out even when not
        strictly necessary. For example, in

          (a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32

        the sum a + b is expanded. Users may be able to achieve speed-ups
        by first introducing abbreviations and then proving general forms,
        e.g.

          x <+ c /\ c <+ d ==> x <+ d:word32

        The conversion handles most operators, however, the following are
        not covered or interpreted:
           + Type variables for word lengths, i.e. terms of type ``:'a
             word``
           + General multiplication, i.e. ``w1 * w2``. Multiplication by a
             literal is okay, although this may introduce many additions.
           + Bit field selections with non-literal bounds, e.g. ``(exp1 --
             exp2) w``.
           + Shifting by non-literal amounts, e.g. ``w << exp``.
           + ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w.
           + word_div, word_sdiv, word_mod and word_log2.

New examples:

      * A development of some basic computability theory:
           + a development of λ-terms as computable functions, showing that
             things like Church-numerals are as powerful as one would like,
             and that λ-terms can indeed be set up to evaluate suitably
             encoded λ-terms (thereby providing a Universal Machine);
           + a development of primitive recursive and recursive functions
             doing much the same;
           + a demonstration that both models can emulate each other;
           + definition of concepts of recursive, and
             recursively-enumerable sets; and
           + some standard results, including: the Halting Problem, Rice's
             Theorem, the Recursion theorem, that recursive sets are closed
             under union and complementation, that r.e. sets are closed
             under union and intersection but not complement, and that if a
             set and its complement are both r.e. then they are both
             recursive.

Incompatibilities:

      * Drule.CONJUNCTS_CONV (proving equivalence of conjunctions under
        associativity, commutativity and idempotence) has been renamed to
        Drule.CONJUNCTS_AC.

      * Drule.CONJ_SET_CONV and Drule.FRONT_CONJ_CONV have been removed.
        Their functionality can easily be derived from Drule.CONJUNCTS_AC.

      * The overload <> on words$word_slice has been removed and replaced
        with ''.

      * The interface of userprinter (user defined pretty printers)
        changed. Instead of getting just two functions add_string and
        add_break, it now gets a record of type term_pp_types.ppstream_funs
        that contains these functions as well as several others.

      * The type of the filter field of the SSFRAG function for
        constructing simpset fragment values has changed from
        (thm -> thm list) option to
        (controlled_thm -> controlled_thm list) option, where a "controlled
        theorem" value is a pair of a theorem and a control indicating how
        many times the rewrite is allowed to be applied. See the REFERENCE
        and the BoundedRewrites module for details.

      * The Unicode structure is now a sub-structure of Parse, due to some
        significant code-reorganisation. This means that a line such as
          open Parse boolLib Unicode

        will fail. Instead it must be

          open Parse boolLib
          open Unicode

      * The constant INFINITE in pred_setTheory has been replaced by an
        abbreviation. Thus, if one types ``INFINITE s``, the underlying
        term is really ¬FINITE s. All instances of this pattern will print
        as INFINITE s. The functions mk_infinite, dest_infinite and
        is_infinite in pred_setSyntax continue to work and do the “right
        thing”, the entrypoint infinite_tm in the same module has been
        removed.
      __________________________________________________________________

    HOL 4, Kananaskis-6

------------------------------------------------------------------------------
This SF.net Dev2Dev email is sponsored by:

Show off your parallel programming skills.
Enter the Intel(R) Threading Challenge 2010.
http://p.sf.net/sfu/intel-thread-sfd
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

STACS 2011 - Last Call for Papers

************************************************************************
28th International Symposium on Theoretical Aspects of Computer Science

               STACS 2011 - LAST CALL FOR PAPERS

               March 10-12, 2011, Dortmund, Germany

             Deadline for submission:  September 24, 2010
      Submission site: http://www.easychair.org/conferences/?conf=stacs2011

	                       http://stacs2011.de/
************************************************************************

SCOPE
********
Authors are invited to submit papers presenting original and
unpublished research on theoretical aspects of computer
science. Typical areas include (but are not limited to):

* Algorithms and data structures, including: parallel and distributed
  algorithms, computational geometry, cryptography, algorithmic learning
  theory;
* Automata and formal languages;
* Computational and structural complexity;
* Logic in computer science, including: semantics, specification, and
  verification of programs, rewriting and deduction;
* Current challenges, for example: biological computing, quantum
  computing, mobile and net computing.

PROGRAM COMMITTEE
***************************
Dietmar Berwanger, ENS Cachan
Patrick Briest, Paderborn University
Christian Choffrut, LIAFA, Université Denis Diderot 
Benjamin Doerr, MPI Saarbrücken
Christoph Dürr, Ecole Polytechnique  (co-chair)
Leah Epstein, University of Haifa
Thomas Erlebach, University of Leicester
Michele Flammini, University of L'Aquila 
Nicolas Hanusse, LaBRI Bordeaux
Markus Holzer, Gießen University
Dániel Marx, Tel Aviv University
Claire Mathieu, Brown University
Colin McDiarmid, Oxford University
Rolf Niedermeier, Jena University
Nicolas Ollinger, Aix-Marseille Université
Marco Pellegrini, CNR Pisa
Jean-Francois Raskin, Université Libre de Bruxelles
Thomas Schwentick, TU Dortmund University (co-chair)
Jeffrey Shallit, University of Waterloo
Till Tantau, University of Lübeck
Sophie Tison, Université de Lille
Ronald de Wolf, CWI Amsterdam

INVITED SPEAKERS
****************
- Susanne Albers, Humboldt University Berlin
- Veronique Cortier, LORIA Nancy
- Georg Gottlob, Oxford University

SUBMISSIONS
***********
Authors are invited to submit a draft of a full paper with at most 12
pages (STACS style or similar - e.g. LaTeX article style, 11pt
a4paper) at
             http://www.easychair.org/conferences/?conf=stacs2011.

The title page must contain a classification of the topic
covered, preferably using the list of topics above. The paper should
contain a succinct statement of the issues and of their motivation, a
summary of the main results, and a brief explanation of their
significance, accessible to non-specialist readers. Proofs omitted due
to space constraints must be put into an appendix to be read by the
program committee members at their discretion. Submissions deviating
from these guidelines risk rejection. Electronic submissions should be
formatted in PDF.

Simultaneous submission to other conferences with published
proceedings is not allowed.

PROCEEDINGS
***********
Accepted papers will be published in the proceedings of the Symposium.
As usual, these proceedings will appear in the Leibniz International
Proceedings in Informatics (LIPIcs) series, based at Schloss
Dagstuhl. This guarantees perennial, free and easy electronic access,
while the authors will retain the rights over their work.  In
addition, the proceedings will also be available as archives in the
open access electronic repositories HAL and arXiv. With their
submission, authors consent to sign a license authorizing the program
committee chairs to organize the electronic publication of their paper
if it is accepted. Further details are available on www.stacs-conf.org
and on the conference website, stacs2011.de. 

Instructions for the preparation of final manuscripts can be found at
the LIPIcs website:
http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/. 

Participants of the conference will receive a USB-stick with an
electronic version of the proceedings.  It is also planned to publish
in a journal a selection of papers.

IMPORTANT DATES
***************
Deadline for submission:  September 24, 2010
Notification to authors:  November 29, 2010
Final version:              January 3, 2011
Symposium:                March 10-12, 2011

------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing
http://p.sf.net/sfu/novell-sfdev2dev

Call for Paper: TLCA'11, 1-3 June 2011, Novi Sad

CALL FOR PAPER
TLCA 2011, 1-3 June 2011, Novi Sad

 http://www.rdp2011.uns.ac.rs/tlca/index.html

The 10th Conference on Typed Lambda Calculi and Applications (TLCA
2011)  is a forum for original research in the theory and applications
of typed lambda calculus, broadly construed. Suggested, but not
exclusive, list of topics for submission are:
    * Proof-theory: formal reasoning based on type theory, linear
      logic and proof nets, type-theoretic aspects of computational complexity
    * Semantics: game semantics, realisability, categorical and other models
    * Types: dependent types, polymorphism, intersection types and
      related approaches (union types, refinement / liquid types, 
      behavioural types), type inference, types in program analysis and verification
    * Programming: foundational aspects of functional and
      object-oriented programming, flow analysis of higher-type computation,
      program equivalence (step-indexed, bisimulation and related methods)

IMPORTANT DATES
---------------
26 January 2011:  Submission of titles and short abstracts
2 February 2011, 23:00 Greenwich Mean Time:    
           Strict deadline for submission of 15-page full papers
23 March 2011:  Notification of acceptance
3 April 2011:   Camera-ready paper versions due
(The above dates are tentative, to be confirmed as soon as possible.)

Programme Committee Chair

    * Luke Ong (Oxford, GB)

Programme Committee

    * Thorsten Altenkirch (University of Nottingham)
    * Stefano Berardi (University of Torino)
    * Adriana Compagnoni (Stevens Institute of Technology, New Jersey)
    * Giles Dowek (Ecole Polytechnique, Paris)
    * Silvia Ghilezan (University of Novi Sad)
    * Hugo Herbelin (INRIA, Paris)
    * Atsushi Igarashi (Kyoto University)
    * Ranjit Jhala (UC San Diego)
    * Ralph Matthes (CNRS, IRIT)
    * Ugo dal Lago (University of Bologna)
    * Luke Ong (University of Oxford) (PC Chair)
    * Rick Statman (Carnegie Mellon University)
    * Tachio Terauchi (Tohoku University)
    * Nobuko Yoshida (Imperial College, London)

TLCA Publicity Chair

      * Luca Paolini (Turin)

------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing.
http://p.sf.net/sfu/novell-sfdev2dev

HOL Light installation on Mac OS X 10.6.4

Hello,

I've been unsuccessful in installing HOL Light on my Mac. I have both
OCaml 3.12.0 and camlp5 5.15 installed, and I'm installing from the HL
snapshot of 10 January 2010 from the HOL Light page, but when I type
'make' in the hol_light directory, I receive the message:

if test `ocamlc -version | cut -c1-4` = "3.10" -o `ocamlc -version |
cut -c1-4` = "3.11" ; \
                   then ocamlc -c -pp "camlp5r pa_lexer.cmo
pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
                   else ocamlc -c -pp "camlp4r pa_extend.cmo
q_MLast.cmo" -I +camlp4 pa_j.ml; \
                   fi
File "pa_j.ml", line 104, characters 10-13:
Parse error: "::" or "]" expected after [sem_expr_for_list] (in [expr])
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2

Thinking that it might have worked despite the error, I typed #use
"hol.ml";; while in OCaml. I obtain

val hol_version : string = "2.20++"
val hol_dir : string ref = {contents = "/Users/Anthony/Documents/hol_light"}
val temp_path : string ref = {contents = "/tmp"}
Exception: Symtable.Error _.

Would anyone be able to help?

Many thanks in advance,

Anthony Pulido

------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing.
http://p.sf.net/sfu/novell-sfdev2dev