Re: [Hol-info] Visualizing subgoals in a proof script

[Freek Wiedijk]

Dear Mario,

>Hello. In HOL4 is there a way to generate something like the entries in
>Metamath proof explorer for the subgoals generated within a proof and
>the tactics used to solve them? Example:
>

For HOL Light there is Mark Adams's "tactician" which
I expect would make something like this possible (even
though I expect it only would work on the majority of
proofs, and not be guaranteed to work on all of them).
But that's HOL Light, not HOL4.

Freek


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Installation Problem of HOL-Light

[Freek Wiedijk]

Dear all,

Some time ago (in the times of Debian Stretch :-)) I made
a Dockerfile for HOL Light, see the attachment.

The commands I used for building the image and running
it are:

  docker build -t hol-light .
  docker run -i -v /home/freek:/home/freek --name hol-light hol-light

You need to run the build command in the directory (".") that
has the Dockerfile in it.  Of course, the directory you
want to mount in the container in your case probably will
not be /home/freek :-)

Then at the ocaml prompt ("# ") when running the image,
I input some ocaml commands:

  #use "hol.ml";;
  loads "update_database.ml";;
  #load "unix.cma";;
  let cd path = Unix.chdir path;;
  let pwd () = Unix.getcwd ();;
  let ls () = Unix.system "/bin/ls -C";;
  cd "/home/freek";;
  ls ();;

I have Docker checkpointing enabled
in my /etc/docker/daemon.json, see
https://docs.docker.com/engine/reference/commandline/checkpoint/,
so in a different window I then gave the command:

  docker checkpoint create hol-light hol

This creates the checkpoint.  Finally, I then run HOL Light
every time using:

  docker start -i --checkpoint hol hol-light

It still takes some time to start, but you don't have
to go through the initialisation of the system with #use
"hol.ml";; every time...

Unfortunately, you cannot have two instances of this running
at the same time.  If someone can tell me how to do that
(I'm not really a Docker user), I would appreciate that.

Even if you don't want to use docker, the Dockerfile shows
commands to install the system in a way that works :-)  I
_think_ I even tested that the SOS stuff works in this setup.

Hope this is useful to someone.

Freek
FROM debian:stretch-slim
RUN \
apt update && \
DEBIAN_FRONTEND=noninteractive apt-get -yq install \
  ocaml camlp5 git make coinor-csdp && \
cd /usr/src && \
git clone https://github.com/jrh13/hol-light.git && \
cd hol-light && \
make
WORKDIR /usr/src/hol-light
CMD /usr/bin/ocaml
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Freek Wiedijk]

Dear all,

For what it's worth, a definition of division with 0/0 = 0
won't be possible constructively, because in constructive
mathematics all functions of type real->real are continuous,
and with this definition division is _not_ continuous.

Also, in IEEE 754 floating point of course division is a
total operation.  One can easily imagine an "extreal" type
that is in this spirit (with "infinity" and "-infinity"
and "nan" added to the mathematical reals), where division
is total.

Finally, my PhD advisor Jan Bergstra has a theory of
something called "meadows" (related to "fields", I guess),
in which division is total.  Google "bergstra meadows"
for some references :-)  So that gives some legimity
to formalizing a total division function ("this is just
about meadows").  I never really looked at this work though,
and don't know whether in "meadows" one always has 1/0 = 0.
(I guess one certainly will have 0/0 = 0.)

I'm sure all these observations won't satisfy traditional
mathematicians about the treatment of divisions in systems
that only allow for total functions.  Hell, it doesn't
statisfy _me_ :-)

Freek


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Tactic

[Freek Wiedijk]

Hi Dylan,

What I would try in HOL Light:

# g `a ==> b /\ c ==> d /\ e ==> k`;;
Warning: Free variables in goal: a, b, c, d, e, k
val it : goalstack = 1 subgoal (1 total)

`a ==> b /\ c ==> d /\ e ==> k`

# e (REPEAT DISCH_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`a`]
  1 [`b /\ c`]
  2 [`d /\ e`]

`k`

# e (POP_ASSUM_LIST (MAP_EVERY (MAP_EVERY ASSUME_TAC) o rev o map CONJUNCTS));;
val it : goalstack = 1 subgoal (1 total)

  0 [`a`]
  1 [`b`]
  2 [`c`]
  3 [`d`]
  4 [`e`]

`k`

# 

Freek

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Freek Wiedijk]

Hi Jeremy,

>My dominant recollection is the difficulty of getting the system to do the
>right type inference, and getting terms to typecheck.  I was forever working
>out where I needed to put in type annotations.

In Coq and Mizar I don't have this experience, in the sense
that I hardly ever need type annotations where I don't expect
them.  In occasionally have problems with "match ... with
..." typing, getting that to work can be very frustrating.
But apart from that, I don't have much of a problem.

>It led me to conclude that the systems offering automatic inference of a
>principal type really occupy a "sweet spot", ie the best compromise between
>ease of use and expressive power.

I don't mind so much explicitly typing my variables
where they are bound.  So I don't share this feeling of
Hindley-Milner style polymorphism being a "sweet spot".
I'd rather have full polymorphism and dependent types
as well.

Freek

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Experience and opinions on proof assistants with “rich” type systems

[Freek Wiedijk]

Hi Ramana,

>Perhaps it would make more sense to ask people who are using rich type
>systems what their motivations are :)
>(On this list it's probably mostly people who are satisfied with simple
>type theory.)

One can do everything with anything.  So dependent tpes
certainly are not _needed_ for formalization.  But dependent
types _are_ very convenient.  I know them both from Coq
and from Mizar.

In Mizar the foundations are untyped ZF-style set theory
(Josef Urban's PhD thesis is about cooking away all the
syntactic sugar), so you don't need an "an enormously
complex logic" (Mario's words) to get dependent types.

Examples of types that to me seem dependent in a natural
way are, in mathematics:

  element of the set X
  element of the carrier of the algebraic structure X
  vector space of dimension n
  normal subgroup of group G
  field of characteristic p
  field extension of field K
  simplicial k-complex
  morphism from A to B in a category

and in (theoretical) computer science:

  array of length n
  integer of signedness s and size n
  machine program of processor architecture P
  C program of implementation I
  normal form of term t under some reduction relation
  term of type A in a typed system

or in mathematical logic:

  proposition over a signature S
  proof of proposition A

Etcetera, etcetera.

The last actually _also_ has the signature S as an argument,
but it is "hidden" (implicit) because it can be inferred
from the type of A, so does not need to be written.
These implicit arguments are quite powerful.  For example,
when working in group theory, you can write x + y, but
actually it will be a ternary operation, with the group the
third argument that can be inferred from the type of x and y.

I know that John Harrison has a hack where he uses
type variables to simulate natural numbers, and you get
_something_ like dependent types in HOL that way.  But that
really only goes so far.

Now various of these types are sometimes in a natural way
empty (for example the type "normal form of term t", when t
does not have a normal form), which makes it so irritating
that Mizar doesn't allow for empty types.  Without dependent
arguments, not allowing for empty types is not a big deal
(like in HOL), but once you ahve dependent types you really
also have to allow for types being empty.

Even when you don't care at all (like I do, well maybe :-))
for the Curry-Howard isomorphism.

Freek

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Emacs Macros for HOL Light Proof

[Freek Wiedijk]

Hi Rob,

>>[...] and Freek Wiedijk's vi mode for HOL Light.
>Where do I find the above-mentioned vi mode?

The current version has been on the web for a while at

  

but there is no link yet.  Everyone should feel free to
do with it whatever they like.  I haven't checked whether
it's still compatible with the latest version of HOL Light
(or vim, for that matter).

There is a README with some explanations that I wrote
for John (but as he's not a vi user, I'm not sure he has
tried it.)

This is very much not a polished thing.  I never used it
to write a significant HOL Light formalization.  I'm sure
that if I would, the commands for the thing (and maybe its
behavior) would change significantly.

This is an attempt to make something that behaves like
interfaces like Proof General and CoqIDE and so on for HOL
Light.  I.e., one edits a file, and in a separate window
a proof state is updated simulaneously that corresponds to
a location in the file, without having to even think about
commands being processed in a HOL Light session.  So there
is no concept of "copying from the file to a session".
The file itself contains the proofs and proof steps, and
that's just it.

This only works for HOL Light proofs in "John Harrison style"
(but of course can be adapted for different styles.)

It also works on the lemma level, so it doesn't know about
the file as a whole, it only knows about a single lemma
at the time (a lemma being defined as a part of the file
between two successive empty lines.)

It imitates the Matita interface where one can step throught
a ... THEN ... THEN ... chain that works on multiple subgoals
simultaneously (in Coq terms: "also steps semicolons".)

It's very "hacky", with communication through the file
system (in /tmp), and with vi sessions talking to each
other, and so on.  I'm sure it can be organised better
(named pipes? I kind of dislike that kind of thing),
but am not really interested in trying to work on such a
reorganised version myself.  It also probably is easy to
adapt this for emacs.

Myself, I really like this interface.  I'm sure that _if_
you want to use HOL Light in John's style, and _if_ you
want to use vi (vim) as your editor, and _if_ this gets a
bit more work, it really would be a helpful interface.

And I would _love_ to see a HOL4 version of this :-)

Freek

--
Presto, an open source distributed SQL query engine for big data, initially
developed by Facebook, enables you to easily query your data on Hadoop in a 
more interactive manner. Teradata is also now providing full enterprise
support for Presto. Download a free open source copy now.
http://pubads.g.doubleclick.net/gampad/clk?id=250295911=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Viewing HOL proofs

[Freek Wiedijk]

Ramana:

For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is
perhaps even better for interactive proof-viewing, since it also keeps
track of where you are up to in the editor buffer, and shows all subgoals
of the proof in the viewing terminal.

FWIW, this thing I developed for my own use, and I have
hardly used it myself yet either.  It also is a big hack.
OTOH, I kind of like it, and anyone who wants to try it
can have it, just mail me.

What it is, it is a thing for HOL Light that clones the user
experience of the Proof General/CoqIDE/etc way of working
with proofs.  You can step through HOL Light proofs as long
as you use John's prove(`...`, ... THEN ... THENL ...) style
(and I guess you can hack it to work for different styles
too).  So the proof will have been processed up to a certain
point, and the goal at that point is shown in a different
window.  As it is low-tech vi, there's no highlighting,
instead the current location in the proof is marked with a
|# sign.  But one doesn't need to copy-paste from one
window to another, one just edits in the final file, and
it gets processed.

The thing can step through multiple goals in parallel (in
Coq words it can stop at semicolons too), when a tactic
produces multiple goals but one doesn't do a THENL then.
This is something I first saw in Matita, and that I liked,
so I imitated that.  It means it behaves different from the
normal interactive way of using HOL Light, as in that case
you always only work on one goal at the time.  The interface
also can show the goals you're not working on right now
(although you can turn that off too, if you don't want to
be bothered).

Freek

--
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the 
conversation now. http://goparallel.sourceforge.net/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Undefined operations such as division by zero in HOL

[Freek Wiedijk]

Hi Mike,

Taking definedness to the level Freek is discussing would,
I think, not let you prove that

  x DIV 0 = x DIV 0

Exactly.  I think that what I want is much closer to PVS and
B than to IMPS.  I also don't want any change to the logic.
I _hate_ partial logics.  I want to be able to use all the
tools that are available for the (standard) total logics!

As I say, I _hate_ partial logics.  You get multiple variants
of equality.  With one you can prove `1/0 = 1/0`, with one
you can _dis_prove `1/0 = 1/0`, and maybe you even have
other ones too?  So I want a world in which writing
`1/0 = 1/0` is _illegal_ (something akin to a type error).

_And_ want that `!x. 1/x = 1/x` is illegal too (because x
can take the value 0), but I _also_ want that
`!x. ~(x = 0) == 1/x = 1/x` is fine (even although x
_still_ can take the value 0).  That's how things work in B.
And this seems unlike IMPS to me.

What I just want is to have some story + infrastructure
that allows me to -- at the very very end -- prove that
the result that I have established is meaningful, in the
sense that it doesn't depend on/refer to what functions do
outside their domain.  But that apart from that _everything_
is as it was before.

Freek

--
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis  visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Undefined operations such as division by zero in HOL

[Freek Wiedijk]

Hi Rob,

Given a Z specification it could generate a set of proof
obligations called domain conditions. The idea was that
if the domain conditions were true, then the specification
was insensitive to the interpretation of undefined terms.

This is exactly what I was trying to describe, and the way
things currently work in B as well, I think.  (Of course
B is very closely related to Z).

It ought to be feasible to do something similar for HOL.

Ah, that sounds good!  So I just am looking for a principled
account of what a reasonable definition of those domain
conditions are in the HOL logic.  I think.

Given that in HOL the logical connectives are defined in
terms of more primitive notions like equality, you would
like to have a calculus that gives you reasonable domain
conditions for those logical connectives, based on how
they are defined for terms that are just written in terms
of equality.

Freek

--
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis  visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Learning HOL Light

[Freek Wiedijk]

Vincent:

Then each time you type something that starts with a semi-colon (e.g., 
`;blabla`), you obtain the intermediate preterm instead of the term.

Hey!  miz3 already uses `;...` for proofs.  So maybe it's
less confusing if you use another symbol to get preterms?

Freek

--
Own the Future-Intel(R) Level Up Game Demo Contest 2013
Rise to greatness in Intel's independent game demo contest. Compete 
for recognition, cash, and the chance to get your game on Steam. 
$5K grand prize plus 10 genre and skill prizes. Submit your demo 
by 6/6/13. http://altfarm.mediaplex.com/ad/ck/12124-176961-30367-2
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Fixing HOL Light

[Freek Wiedijk]

Phil:

When a theorem is proven and HOL Light announces no
subgoals, there is no jingle. or musical fanfare. Please
fix.

How about?

let e tac =
  let gs = refine(by(VALID tac)) in
  match gs with
  | (_,gls,_)::_ -
if length gls = 0
then let _ = Unix.system (mpg123 -q ^(!hol_dir)^/ahhh.mp3) in gs
else gs
  | _ - gs;;

(I'm sure this can be shorter, but who cares.)

For the sound file (which you need to put in the HOL Light
directory): http://www.cs.ru.nl/~freek/pics/ahhh.mp3

Bonus points for people who know where this sound came from.

Freek

--
Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS
and more. Get SQL Server skills now (including 2012) with LearnDevNow -
200+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only - learn more at:
http://p.sf.net/sfu/learnmore_122512
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

Can you jump into the discussion Michael and I were having
about whether miz3 is intentionally weakened?  Michael seems
to think yes, I think no, but I wonder what effect the MESON
depth limit of 50 has, or the fact that MESON is just FOL
and not HOL.

Ah no, there were no deep thoughts behind the choice of by
in miz3.  I just chose the most trivial option available
(well, also I wanted it to be at least as strong as the
real Mizar by...  which it isn't, because you lack the
properties and requirements.)

As I wrote before, I think the thing actually is bad,
because often you can justify a proof step with a REWRITE_TAC
that only does a very small number of rewrites, but not
with the default by.  That feels very strange.

Implementing a better by for miz3 is a nice project to
think about, but it's not on the top of the stack of things
I'm currently considering doing.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

Thus, I conclude that the purpose of the default timeout
isn't to weaken miz3, but to better instruct beginners

Ah no, the main point was that if an inference is _not_
correct, often MESON will run for the full timeout time.
So checking proofs with errors (= all proofs when you're
not finished yet) gets very slow, and without timeout close
to infinite.  The timeout thing is just to deal with that.

I think the original Automath from the seventies had
exactly the same feature.  Typechecking in type theory _is_
decidable, but if things are type incorrect, in Automath it
takes forever to establish this (because it will endlessly
unfold all definitions: Automath didn't have opaqueness.)

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

Why are miz3 and Mizar the only proof assistants where
one can easily write up human readable proofs?

I'm surprised you're not including Isar in this list!

And do you know about ForTheL (see
http://nevidal.org/download/forthel.pdf)?  Now _there's_
a readable formal language! :-)

Also, does anyone know what is the status of Mohan
Ganesalingam's work in this direction (see for example
http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf)?

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL and the axiom of choice

[Freek Wiedijk]

Hi Rob,

   (exists f. forall x. P(x, f(x))) = (forall x. exists y. P(x, y))

So _this_ is the kind of choice that I have no problems with,
as it doesn't threaten my Platonism.  (It is even provable
in type theory!  (But only if you use the right flavor of
existential quantifier of course :-)))

I once heard a very interesting talk by Per Martin-Löf
about the axiom choice, see
http://www.math.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf.
I think he was making the point then that AC really is
a confusion between two different principles that _are_
valid if you're a type theorist.  (Of course those
two principles _don't_ give you AC if you're working in a
set theoretical setting :-))

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL and the axiom of choice

[Freek Wiedijk]

Hi Cris,

At a philosophical level I'm surprised that Freek's
intervals of Platonism are during the week, with formalism
on weekends.

It was a reference to a book related to the philosophy
of mathematics that I liked a lot when I was much younger.
See the quote on
http://www.homodiscens.com/home/areas/math_certainty/platonists/.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL and the axiom of choice

[Freek Wiedijk]

Hi Cris,

To chime in on this:

I don't have any problems with a system that doesn't allow
you to disable the axiom of choice.  In other words:
hardwire choice all you like as far as I'm concerned.
Without AC you get weirdnesses as that a union of countably
many countable sets doesn't need to be provably countable.
Who would like to reason in such a weak system :-)

I know, keeping track of where you used AC in a proof
is a fun game, and textbooks sometimes do this too.
But _mathematically_ it doesn't seem _too_ interesting to me.

However, I _do_ have problems with HOL's choice operator!
Mainly this is for philosophical -- i.e., for not very good
-- reasons.  See, I'm a Platonist (that is to say: during
the week; in the weekend I'm a formalist :-))  So when I
think about mathematics, I imagine a space of ZF sets,
where the ZF sets live.  And when writing mathematics I
would like to consider that as pointing at those sets
and talking about them.  (Look, that set there, that's
the natural numbers!)

Now, _without_ Hilbert's choice operator epsilon, every HOL
term clearly denotes at a welldetermined set.  (That is, if
you fix some straight-forward set theoretic encoding of the
HOL universe.)  However, once you add the epsilon, that's
no longer true.  It then depends on _what_ choice operator
you choose, what the set is that you are talking about.
And it's not clear how to (Platonically!) distinguish one
choice operator from the other.  Therefore once you write
HOL terms that contain an epsilon somewhere, _I_ don't know
(Platonically!) anymore what they mean.

So the choice operator in HOL always makes me a bit uneasy.

Not that it really matters of course.  And a choice operator
_is_ a really useful thing to have :-)

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Michael,

miz3's by is just an invocation of MESON but with,
as I understand, a time limit imposed.

FWIW, one can turn off the time limit by setting timeout
to -1.  This is useful for example if one wants to recheck
a proof that is known to be correct on a slow computer.

Of course, if a miz3 proof contains a tactic that doesn't
terminate, then with this setting the checking of that
proof won't terminate either.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

MESON[]
`(!x y z. P x y /\ P y z == P x z) /\
(!x y z. Q x y /\ Q y z == Q x z) /\
(!x y. P x y == P y x) /\
(!x y. P x y \/ Q x y)
== (!x y. P x y) \/ (!x y. Q x y)`;;

MESON solves this logic puzzle (which I still haven't yet
solved) quite quickly, and it writes
...solved at 23107


let LosLogic_THM = thm `;
  let x y be A;
  let P Q be A-A-bool;
  assume ! x y z. P x y /\ P y z == P x z [H1];
  assume ! x y z. Q x y /\ Q y z == Q x z [H2];
  assume !x y. P x y == P y x [H3];
  assume !x y. P x y \/ Q x y  [H4];
  thus (!x y. P x y) \/ (!x y. Q x y)

  proof
  qed by H1, H2, H3, H4`;;

The miz3 proof is almost as quick, with a MESON `solved at'
number of 23088.

Actually 23088 is _smaller_ than 23107, so I don't know
what you mean with almost as quick :-)

I have been trying to understand where the difference between
23107 and 23088 comes from.  The reason is that MESON gets
as its argument a list of thms corresponding to H1 until H4,
instead of getting them as antecedents of an implication:

# MESON
[ASSUME `!x:A y:A z:A. P x y /\ P y z == P x z`;
 ASSUME `!x:A y:A z:A. Q x y /\ Q y z == Q x z`;
 ASSUME `!x:A y:A. P x y == P y x`;
 ASSUME `!x:A y:A. P x y \/ Q x y`]
`(!x:A y:A. P x y) \/ (!x:A y:A. Q x y)`;;
0..0..2..7..16..30..48..72..108..168..236..340..516..702..918..1260..1660..2098..2716..3438..4298..5528..6944..8594..11052..13780..16742..20862..solved
at 23088val it : thm = !x y z. P x y /\ P y z == P x z,
  !x y z. Q x y /\ Q y z == Q x z, !x y. P x y == P y x,
  !x y. P x y \/ Q x y |- (!x y. P x y) \/ (!x y. Q x y)
# 

So there's the 23088 again, see?

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Freek Wiedijk]

Hi Ramana,

In HOL4 that is called PROVE_HYP.

In HOL Light too, thanks for answering my question!
(Its arguments have the opposite order from the function
I wrote though :-))

In HOL4 you can control how much assumptions are printed
with a trace called assumptions,

HOL Light just prints them in full, I think.  Ah well,
as I already wrote, this way of working does not appeal
too much to me anyway :-)

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Freek Wiedijk]

Hi Ramana,

Later, after a long exploratory theory development, having settled on the
right structures, you can go back and fill in the cheats with real proofs,

Yes, for example Peter Aczel was arguing for this once too,
I think.  It's a tempting approach.

But my experience is that whenever I try to do this kind
of thing I get it wrong.  I.e., when I finally go back, I
find that it turns out not to be provable what I interpolated
there (because I forgot about certain necessary hypotheses,
for example), and that I have been building on quicksand.

It might be that others are more precise than me, so that
this is a personal problem.

And it also might be the case that it still is not _too_ bad
this way, that it still is relatively easy to repair things.

But this oh my, that's not provable after all! feeling was
so much a turn off to me, that I stopped trying to work in
this style.  Nowadays, I just prove things in their proper
order, and all of it.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Freek Wiedijk]

Hi Cris,

I was speaking from a software engineering and usability
point of view.

Okay, just to fix our minds: would you consider Knuth's/
Lamport's latex to be usable in this sense?  Because I
would strongly claim that it is.  It's one of the most
usable systems I know.

That's why I think that Mark's focus on things like error
messages and concrete syntax is missing the point.  Latex is
pretty horrible in that respect, but _that doesn't matter._

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants for way more people

[Freek Wiedijk]

Hi Mark,

It's just that no-one's done it yet!

There are just two things that make proof assistants
difficult to use:

1. There is not sufficient automation of trivial stuff.

   I.e., you generally need to break down your reasoning into
   smaller steps than how you would experience things when
   you wouldn't be dealing with a proof assistant.  Maybe you
   _would_ experience those steps very fleetingly, but you
   wouldn't focus at them in the way a proof assistant
   forces you to.  It's like doing math vr
   slllwwlyyy.

   If some step in a proof is obvious to you, you want to be
   able to just say well, that's obvious and nothing more.
   That's unfortunately not how it seems to work right now.
   Even if there's automation in a system that can solve
   such a problem, you need to be aware _what_ automation
   to invoke.

2. You need to be able to find things in a library, or
   establish that the thing you think you need is not
   there yet.

   And you need to be able to keep your library
   well-organised and in sync with the versions of your
   systems.  Not easy.

   Random example: suppose you want to use Schwarz's
   inequality in a proof.  So _here's_ your formalisation
   that you're working on, and _there's_ the library of your
   system.  Now what?  You will need to give search commands,
   or switch windows to look at lists of things you might
   need, or try to remember what the lemma was called and
   what was its exact shape... it's all irritating overhead.

   And when you prove something you will need to decide
   on a name for your new lemma.  That's something that's
   particularly difficult.

There are no other reasons proof assistants are difficult.
So will these be the two things you'll be addressing?

Of course these two things are related.  And Sledgehammer
clearly is trying to address these problems.  But yes,
it's not fully done yet.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proof assistants and high school math

[Freek Wiedijk]

Hi Grant,

Are you familiar with Michael Beeson's MathXpert (formerly MathPert)?

Yes, MathXpert-level mathematics is exactly what I had in
mind when I was talking about high school mathematics.

The main difference between what MathXpert provides and what
I was asking for, is that MathXpert is about simplifying
expressions and solving equations, while what I was asking
for is also to establish whether some statement (equation
or inequality) follows from other statements.

I seem to remember that Michael claimed to me at some time
that MathXpert could do that kind of thing too without too
much extra work, but I would have to see how that would
turn out.

Another way to characterize this kind of high school
mathematics is reasoning about equationsa and inequalities
that have been written using the operations that are standard
in Content MathML.

Of course the development of MetiTarski is all about this
issue too.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill  John,

| Better error messages would be great.

The way the error messages work is that first the proof is
split into steps based on the semicolons and keywords.
(I think certain keywords always start a new step and
semicolons always end one, with now and proof being
the exception because they count as a step but don't have a
semicolon, and with bracketing taken into account, because
you don't want to have REWRITE_TAC[FOO; BAR] split the step.)

Anyway, then the errors always point at the end of such
a step.  And then errors 4 to 9 you should take to mean
something is seriously wrong, of the order of a syntax
or type error, while for errors 1 to 3 you should think
about the actual proof, i.e., they mean something like
the contents of the statements don't match up.  Error 3,
skeleton error, means that the proof step doesn't match
the thesis, while errors 1 and 2 mean that the by
didn't get it (or that the inference just doesn't hold in
the first place).

There actually are three parsers working together: my
Mizar-style proof language parser (error 9), the HOL term and
type parsers (error 8) and the ocaml parser for the items
in a by list (which may be thms/tactics/conversions,
so everything there is first given to the ocaml parser:
that's error 5).

I'll defer to Freek on miz3-specific things, but I will try to
improve cases where the native HOL Light error reporting is part of
the problem.

The main problem on that side is of course that the HOL
term parser won't point out where the syntax error is if
there is a syntax error.  Still I don't know whether adding
something for that would be too useful.  If I get error 8,
I generally put the offending statement between backquotes
in the HOL session, and fiddle with it until it's right.
And then copy/paste it back.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

Freek's miz3 code in the miz3 dox 1201.3601-1.pdf
solving the drinker's paradox on p 13--14 is perhaps designed to show
various features of miz3, but it is more than twice as long as needed:

It's mainly intended to be as close as possible to the
Jaśkowsky/Fitch-style natural deduction proof that's right
before it, to show off the similarity of the proof styles.
That one you _can't_ make significantly shorter, because only
the basic natural deduction intro and elim rules are allowed.

But if you want to be short, then

let DRINKER = thm `;
  let P be A-bool;
  thus ?x. P x == !y. P y`;;

already works.  Getting a short proof, or even a proof
that mimics how a human would understand this, was not
the primary aim of the example.  And yes, showing off the
various miz3 proof steps _was_ one of its aims.

If you like to see a _really_ involved proof of this
statement, then look at

http://www.cs.ru.nl/~freek/notes/drinker.miz

Now that's a silly version, as Mizar also can prove this
without any help.  But this one would also work in a minimal
logic version of Mizar :-)

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Mizar Light and miz3

[Freek Wiedijk]

Hi Felix,

However, I discovered the following curious effect: The steps that
previously failed without REWRITE_TAC can also be solved using *only*
GOAL_TAC. For example, in the proof I posted a while ago, the following
step will work.

(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then 1
else 0)) [6] by GOAL_TAC,FUN_EQ_THM;

However, if I drop GOAL_TAC it will fail with an inference time-out. But
if I understood you correctly, then GOAL_TAC does nothing but logging of
the relevant subgoal, correct? So what is going on here?

The reason is that HOL_BY really tries to _solve_ the
goal, so without leaving subgoals.  However, if you give
a tactic yourself, it is allowed to produce subgoals.
These subgoals then have to be trivially solvable by the
statements that are referred to in the by list, and this
last process uses some variant of REWRITE_TAC, I think.

So, if you just put ALL_TAC, the do nothing tactic
(which is what GOAL_TAC really is:

  let GOAL_TAC g =
current_goalstack := (mk_goalstate g)::!current_goalstack;
ALL_TAC g;;

), then effectively you are running some kind of REWRITE_TAC,
which as you observed was good enough.

HOL_BY really needs to be modified in such a way that this
thing doesn't happen.  But how?

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi John,

Then every theorem would become |- TarskiModel((===),Between) == P
instead of just |- P.

Couldn't you set up things in a way that all the theorems
would have the form TarskiModel((===),Between) |- P?
I think I would find that more attractive.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Mizar Light and miz3

[Freek Wiedijk]

Hi Felix,

From what I understand by REWRITE_TAC[FUN_EQ_THM],2 and by FUN_EQ_THM,2
do very different things: by FUN_EQ_THM,2 runs the HOL_BY tactic, whereas
by REWRITE_TAC[FUN_EQ_THM],2 runs REWRITE_TAC, but not HOL_BY. Or does
the second option run first REWRITE_TAC and then HOL_BY?

No, only REWRITE_TAC[FUN_EQ_THM] will be run.

In fact, I would write it myself REWRITE_TAC,FUN_EQ_THM,2.
The tactic in the list after the by can have type thm
list - tactic (in fact, that's the basic ocaml type that
I designed the thing for, a plain tactic is a derived thing.)

I'd find it helpful to have some more verbose error reporting for inference
errors. [...]
If I wanted to implement something like this, where would I start?

Ouch!  I wrote that code some years ago, and would have a
hard time myself doing something like this.  Basically you'd
need to tinker with the whole chain of things:

- think of some syntax for what you want
- adapt the data structures for the proofs to know about
  that syntax
- handle the extra possibilities in the data structures
  when processing the proofs

So the syntax I was thinking about myself was something
like

... by #SOME_TACTIC#,...;

for when you don't want to grow the proof already by
running SOME_TACTIC, but only want to get the subgoals that
get produced by SOME_TACTIC as the current goals in your
HOL session.  To get the goal for a given justification
for working on it then would be

... by ##,...;

I guess.  But I don't know whether I would like something
like this if I tried it.  Maybe I'd hate it :-)

Slightly related: the tactic GOAL_TAC sets the current goal
to the first subgoal produced at a certain point in a proof.
So already you can say things like

... by #SOME_TACTIC THEN GOAL_TAC,...;

or (as a separate proof step)

exec GOAL_TAC;

And then if you in the HOL session do

p();;

you'll see the goal there.

You can even have GOAL_TACs in the middle of a complicated
traditional proof:

... THENL
[...;
 ... THEN GOAL_TAC;
 ...] THEN
...

Sometimes I find that convenient.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi Bill,

I'm pondering the issue of miz3 not allowing free variables
in contrast with how you want to work in an axiomatic
framework.  However, already:

   !(===) (Between:point#point#point-bool) (cong).
TarskiModel((===),(Between:point#point#point-bool),(cong))
 let (===) be point#point-point#point-bool;
let (Between) be point#point#point-bool;
let (cong) be  point#point#point-point#point#point-bool;
assume TarskiModel((===),(Between:point#point#point-bool),(cong)) [0];

The !... line can be avoided by using now.  !x. A == B
proof ...  end; can also be written as now let x be ...;
assume A; ...; thus B; end;.  And then the now can be
omitted if it's on the very outside.  I think.

Also, the assume line doesn't need the typings.  It will be
parsed in the context of the lets.  So you can just write
assume TarskiModel((===),Between,cong); or something in
that style.

But I agree: having these four lines at the start of every
lemma is very unattractive.

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Freek Wiedijk]

Hi John and Makarius,

This is not very much about HOL as such, so if this reply
is inappropriate for the HOL list, I apologise:

mutating the names of constants.

I always found this mutable constants complaint silly.
Many people make it, but it never struck me as significant.

Surely in every practical programming language you can
cheat in some way if you try hard enough.  For instance by
poking the memory, either internally through some Obj.magic
like interface, or if you don't get that from your language
by poking in /dev/mem?

So the possibility of cheating if you really try does not
seem an interesting one to me.  What's important is that
you won't cheat accidentally, by misunderstanding how
things work.

For example there is the story of someone who thought that
some system had a superefficient automated prover, which
made him super excited.  Only later he found out that that
automation had been the system's equivalent of what in
HOL Light is called CHEAT_TAC (adding the thing to be proved
as an axiom.)

In particular, one can generate a proof trace and check
it in a specially designed system like HOL Zero or even
write one's own proof checker. This certainly applies
to HOL Light and Isabelle, with Coq a more arguable
case. (Although it has a small kernel, this involves a
quite complex evaluation mechanism.)

I think Matita started its life that way?  So about Coq
having a small kernel: I seem to remember that the source
of Coq's latest kernel is larger than the source of the
full Mizar system.

Also, I always think that the _full_ logic of Coq (the
thing called pCIC) has nowhere been precisely written down.
If I'm wrong about that, I _very_ much would like to know.
(I know about the Coq manual, but that certainly is not
the full story, nor is it written in a very precise style.)

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Mizar Light and miz3

[Freek Wiedijk]

Hi Felix,

4) I start gvim and load a file with the following content:

let ARITHMETIC_SUM = thm ';
  !n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2
  proof
  qed by #INDUCT_TAC;
';;

The quotes should be backquotes.  With this I think miz3
will try to execute this as ocaml source (it does not match
the pattern of a miz3 lemma).  You can check this theory by
pasting the same text in the ocaml session to see whether
you get the same ocmal error.

Anyway, it should be backquotes.  Proofs are `; ... `
instead of '; ... '

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Mizar Light and miz3

[Freek Wiedijk]

Dear everyone,

John Harrison pointed out to me that the following query was
posted on the hol-info mailing list (I'm subscribed to that
list but often just delete the messages without looking,
sorry about that.  So I missed this):

6) I am very curious about Mizar Light and would like to convert
my exercise to Mizar Light. I found the Mizar Light sources as
well Freek's paper on Mizar Light. However, at first glance it
seemed as if the syntax for Mizar Light given in the paper is
quite different from what I saw in the source. So... what is the
current status of the project?

There have been three experiments that I called Mizar
Light.  However, after some soal searching I decided to
rename the third thing from Mizar Light III to miz3,
so please don't call this third version Mizar Light
anymore... :-)

1. The first thing is described in a TPHOLs paper from
   2001, http://www.cs.ru.nl/~freek/mizar/miz.pdf.
   _Conceptually,_ I still _really_ like this, but
   ergonomically it's completely unusable, because of all
   the quotes and brackets, and because it's really hard
   to debug proofs.  The Mizar proof

 Lm1: P implies P
 proof
   assume P;
   hence P;
 end;

   becomes in this framework:

 let lm1 = prove
  (`P == P`,
   ASSUME_A(0,`P:bool`) THEN
   THUS(`P:bool`) (BY [0][]));;

2. The second version never has been published about, but
   is part of the HOL Light distribution, it is in the
   sub-directory Mizarlight.  It is an attempt to make
   the first version more ergonomic, while still keeping
   the property that a proof is just ocaml code, so without
   having a separate Mizar parser.  In this system the
   above proof becomes:

 let lm1 = theorem
  P == P
  [assume P;
   hence P];;

3. And then there's my recent miz3 system, which
   is my current best effort, and which (very similar to
   John Harrison's Mizar mode) _does_ have a separate
   parser that allows one to get really close to
   Mizar syntax.  It's described in the recent paper
   http://www.cs.ru.nl/~freek/miz3/miz3.pdf,
   and the system can be downloaded as
   http://www.cs.ru.nl/~freek/miz3/miz3.tar.gz.  In this
   system the example is:

 let lm1 = thm `;
  let P be bool;
  thus P == P
  proof
   assume P;
   thus P;
  end`;;

   (In miz3 all variables have to be bound, either in the
   formula or in the context, hence the let at the start.
   Also in miz3 then is implicit, hence the thus
   instead of the hence.)

I hope this clears things up.  I guess the poster might
have been confused between the first and second, or second
and third version of the thing?

Ah yes, and if someone would like help with using miz3,
just mail me!

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Call for bids ITP 2012

[Freek Wiedijk]

It is time to begin the process of selecting a host for ITP 2012, the
International Conference on Interactive Theorem Proving.

Following tradition from TPHOLs, the hosts of the previous conference
(ITP 2011) are running the process. There are two phases: solicitation
of bids and voting. This message concerns the first phase. A
long-standing TPHOLs convention is that the conference should be held in
a continent different from the location of the previous meeting, and
therefore no bids to host ITP 2012 in Europe will be accepted. Based on
ITP and TPHOLs history, ITP 2012 will likely be held in July, August or
September.

Bids should be sent to itp2...@easychair.org and should include at least
the following information:

- name and email address of a contact person
- names of other people involved
- address of website for the bid
- approximate dates of the conference
- structure (e.g., k workshop days and n days of presentations followed
  by excursion...)
- advantages of the proposed venue

An example of a previous winning bid is here:

http://itp2011.cs.ru.nl/ITP2011/Bid_ITP11.html

Deadline for all bids is Monday, 30 May 2011. Shortly after that, the
bids will be made public and the voting phase will take place.  The
people eligible to vote are those who are seriously thinking of
attending ITP 2012. The voting system used will be Single Transferable
Vote between all received bids.

Marko van Eekelen
Herman Geuvers
Julien Schmaltz
Freek Wiedijk

--
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Call for Papers ACL2 2011

[Freek Wiedijk]

 Pierre  (TIMA Labs., France)
Sandip Ray (UT Austin, USA)
David Russinoff (AMD, USA)
Jun Sawada (IBM, USA)
Julien Schmaltz (Open Universiteit, The Netherlands)
Natarajan Shankar (SRI, USA)
Sol Swords (Centaur, USA)
Freek Wiedijk (Radboud Univ. Nijmegen, The Netherlands)

--
WhatsUp Gold - Download Free Network Management Software
The most intuitive, comprehensive, and cost-effective network 
management toolset available today.  Delivers lowest initial 
acquisition cost and overall TCO of any competing solution.
http://p.sf.net/sfu/whatsupgold-sd
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] ITP 2011 (Call for Workshop Proposals)

[Freek Wiedijk]

  Call for Workshop Proposals
   ITP 2011: 2nd International Conference on Interactive Theorem Proving

   22-25 August 2011, Nijmegen, The Netherlands
  http://itp2011.cs.ru.nl/

  -

ITP brings together researchers working in all areas of interactive
theorem proving. The inaugural meeting of ITP was held on 11-14
July 2010 in Edinburgh, Scotland, as part of the Federated Logic 
Conference (FLoC, 9-21 July 2010). The second edition of ITP will 
take place in Nijmegen, The Netherlands, on 22-25 August 2011. 
ITP is the evolution of the TPHOLs conference series to the broad 
field of interactive theorem proving. TPHOLs meetings took place 
every year from 1988 until 2009.

Researchers and practitioners are invited to submit proposals 
for workshops on topics relating to interactive theorem proving. 
Workshops can target the ITP community in general or be focused
to one particular ITP system. 

Possible dates for workshops are 26 and 27 August 2011 (two days after ITP). 
The duration of workshops can be one or two days. 

Important dates:

Submission deadline:13 February 2011
Notification:   13 March 2011

Workshop proposals should be submitted per email to itp2...@easychair.org.

All accepted workshops will be expected to have the programme ready by
July 1st 2011.
 
The workshop selection committee consists of the ITP chairs:

Marko Van Eekelen, Radboud University Nijmegen/Open University of the 
Netherlands
Herman Geuvers, Radboud University Nijmegen
Julien Schmaltz, Open University of the Netherlands/Radboud University Nijmegen
Freek Wiedijk, Radboud University Nijmegen


--
Special Offer-- Download ArcSight Logger for FREE (a $49 USD value)!
Finally, a world-class log management solution at an even better price-free!
Download using promo code Free_Logger_4_Dev2Dev. Offer expires 
February 28th, so secure your free ArcSight Logger TODAY! 
http://p.sf.net/sfu/arcsight-sfd2d
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] ITP 2011 (Call for Papers)

[Freek Wiedijk]

  Call for Papers
   ITP 2011: 2nd International Conference on Interactive Theorem Proving

   22-25 August 2011, Nijmegen, The Netherlands
  http://itp2011.cs.ru.nl/

  -

ITP is the premier international conference for researchers from all
areas of interactive theorem proving and its applications. The inaugural 
meeting of ITP was held on 11-14 July 2010 in Edinburgh, Scotland, as 
part of the Federated Logic Conference (FLoC, 9-21 July 2010).  The 
second edition of ITP will take place in Nijmegen, The Netherlands, 
on 22-25 August 2011. ITP is the evolution of the TPHOLs conference 
series to the broad field of interactive theorem proving. TPHOLs 
meetings took place every year from 1988 until 2009. 


The program committee welcomes submissions on all aspects of
interactive theorem proving and its applications.  Examples of typical
topics include formal aspects of hardware or software (specification,
verification, semantics, synthesis, refinement, compilation, etc.);
formalization of significant bodies of mathematics; advances in
theorem prover technology (automation, decision procedures, induction,
combinations of systems and tools, etc.); other topics including those
relating to user interfaces, education, comparisons of systems, and
mechanizable logics; and concise and elegant worked examples (Proof
Pearls).


Submission details:

All papers must be submitted electronically, via EasyChair:

https://www.easychair.org/conferences/?conf=itp2011

Papers may be no longer than 16 pages and are to be submitted in PDF
using the Springer llncs format.  Instructions may be found at
ftp://ftp.springer.de/pub/tex/latex/llncs/latex2e/instruct/authors/typeinst.pdf
with Latex source file typeinst.tex in the same directory.
Submissions must describe original unpublished work not submitted for
publication elsewhere, presented in a way that users of other systems
can understand.  As for the last edition, the proceedings will be published
as a volume in the Lecture Notes in Computer Science series and will 
be available to participants at the conference.
 
In addition to regular submissions, described above, there will be a
rough diamonds section.  Rough diamond submissions are limited to
six pages and may consist of an extended abstract.  They will be
refereed: they will be expected to present innovative and promising
ideas, possibly in an early form and without supporting evidence.
Accepted diamonds will be published in the main proceedings.  They
will be presented at the conference venue in a poster session.

Authors of accepted papers are expected to present their papers at the
conference, and will be required to sign copyright release forms. 
All submissions must be written in English.

Important dates (midnight GMT):

Abstract submission deadline:   13 February 2011
Paper submission deadline:  20 February 2011
Notification of paper decisions:18 April 2011
Camera-ready papers due from authors:   15 May 2011
Conference dates:   22-25 August 2011

Web page:

http://itp2011.cs.ru.nl/

Invited Speakers:

Don Batory, University of Texas at Austin
Georges Gonthier, Microsoft Research
Mike Kishinevsky, Intel

Conference co-chairs:

Marko Van Eekelen, 
Radboud University Nijmegen/Open University of the Netherlands
Herman Geuvers, 
Radboud University Nijmegen
Julien Schmaltz, 
Open University of the Netherlands/Radboud University Nijmegen
Freek Wiedijk, 
Radboud University Nijmegen

Program Committee:

David Aspinall (Univ. of Edinburgh, UK)
Jeremy Avigad (CMU, USA)
Stefan Berghofer (TUM, Gremany)
Yves Bertot (INRIA Sophia-Antipolis, France)
Sandrine Blazy (IRISA, France)
Jens Brandt (Univ. of Kaiserslautern, Germany)
Jared Davis (Centaur, USA)
Amy Felty (Univ. of Ottawa, Canada)
Jean-Christophe Filliatre (INRIA Saclay, France)
Herman Geuvers - co-Chair (Radboud University Nijmegen, The Netherlands)
Georges Gonthier (Microsoft Research, USA)
Elsa Gunther (UIUC, USA)
John Harrison (Intel, USA)
Reiner Hähnle (Chalmers Univ. of Technology, Sweden)
Matt Kaufmann (Univ. of Texas at Austin, USA) 
Gerwin Klein (NICTA, Australia)
Assia Mahboubi (LIX, France) 
Panagiotis Manolios (Northeastern Univ., USA)
John Matthews (Galois, USA) 
Paul Miner (NASA, USA)
J Moore (Univ. of Texas at Austin, USA) 
Greg Morrisett (Harvard Univ., USA)
Magnus O. Myreen (Univ. of Cambridge, UK)
Tobias Nipkow (TU Munich, Germany)
Michael Norrish (NICTA, Australia)
Sam Owre (SRI, USA)
Christine Paulin-Mohring (Univ. Paris-Sud, France)
Lawrence Paulson (Univ. of Cambridge, UK)
Brigitte Pientka (McGill Univ., Canad)
Lee Pike (Galois, USA)
Sandip Ray (Univ. of Texas at Austin, USA) 
Jose-Luis Ruiz-Reina (Univ. of Sevilla, Spain)
David Russinoff (AMD, USA)
Julien Schmaltz - co-Chair (Open Univ. of the Netherlands, The Netherlands)
Konrad Slind (Rockwell Collins, USA)
Sofiene Tahar (Concordia, Canada)
Marko van Eekelen

[Hol-info] 1 Postdoc and 1 PhD vacancy in the MathWiki project

[Freek Wiedijk]

1 POSTDOC and 1 PHD POSITION in the MathWiki project

   at Radboud University Nijmegen (NL)

   http://www.fnds.cs.ru.nl/fndswiki/Vacancies

The Institute for Computing and Information Science of the Radboud  
University Nijmegen (NL) is looking for 2 researchers to work on the NWO 
project MathWiki a Web-based Collaborative Authoring Environment for 
Formal Proofs.

The vacancies are:

- a POSTDOC for the period of 3 years
vacancy number: 62-16-09


- a PHD POSITION for the period of 4 years
vacancy number: 62-17-09

AIMS OF THE PROJECT
===
The aim of the MathWiki project is to open up to a wider community the 
rich collections of knowledge stored in the repositories of proof 
assistants.

To this end we will build a web-based collaborative authoring 
environment for formal mathematics, the MathWiki system. This system 
will provide interactive web access through a standardized interface to 
a number of proof assistants. The MathWiki system will also be a 
platform for the development of formal proofs within those proof 
assistants and it will provide high level access (through Wikipedia-like 
web pages) to their repositories of formalised mathematics. These 
repositories will reside on the server.

In the project we will study and further develop Wiki technology and 
semantic web technology, all in the context of proof assistant 
repositories of formalized mathematics. The project thus brings together 
the open nature of Wiki authoring with expertise in Proof Assistants and 
Semantic Web technologies to build a new Wiki for mathematics, 
supporting content creation, search and retrieval.

From the perspective of the ordinary user of mathematics, MathWiki will 
be important because it will provide high-level mathematical content on 
the web in a much more coherent and precise way than is available at 
present.

From the proof assistant user perspective, MathWiki will be important 
because it will provide an advanced environment for the collaborative 
authoring of verified mathematics, mediated simply by a web interface.

The MathWiki system will be based on our existing experience with proof 
assistant technology on the web, the ProofWeb systems, see 
http:://prover.cs.ru.nl


-
Requirements for the PhD student position:

- A master's (or equivalent) degree in Computer Science, Mathematics or 
a related field, with a strong interest in proof assistants  and/or 
semantic web technology (preferably both)
- Commitment and a cooperative attitude.
- Very good written and oral English skills.

Requirements for the Postdoc position:

- A PhD in Computer Science, Mathematics, or a related field with 
expertise in proof assistants and/or semantic web technology (preferably 
both).
- A strong publication record.
- Commitment and a cooperative attitude.
- Very good written and oral English skills.

-
Conditions of employment:

The PhD students will be employed for a period of 4 years (40 hrs/week). 
The Postdocs will be employed for a period of 3 years (40 hrs/week). 
Supervision for the projects will be done by Prof. Dr. Herman Geuvers 
and Dr. F. Wiedijk

Postdoc and PhD student will be appointed by the Radboud University 
Nijmegen. Both positions shall start before October 1 2009, but 
preferably earlier.

The salary for the PhD position starts at 2042 Euro per month, 
increasing to 2612 Euro per month in the fourth year.

The maximum salary for the Postdoc is 3755 Euro per month (salary scale 
10).

-
Information:

For more information, see http://www.fnds.cs.ru.nl/fndswiki/Vacancies.
For inquiries about the project and its positions, please contact the 
project leader Prof. Dr. Herman Geuvers (h.geuv...@cs.ru.nl, +31 
243652603). Interested candidates can ask the project leader for the 
complete project application text.


-
Application:

Deadline for application is May 1, 2009.

Send an application letter with CV and 3 references, mentioning the
vacancy number by e-mail to

RU Nijmegen, FNWI, PO
mrs. D. Reinders
Postbus 9010
6500 GL Nijmegen
Netherlands

e-mail: p...@science.ru.nl
telephone: +31 243652764


--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] The QED Project

[Freek Wiedijk]

Dear list members,

A few days ago I got the email copied below.  And I don't
very well know what to say to it.  Does anyone here have
a good answer to Arnold's query?

(I'm cross-posting this to a couple of mailing lists.  So my
excuses for the duplication, but I'm really curious whether
there is anything interesting to say to this question.)

Freek


Message-ID: 4975cdb4.2010...@univie.ac.at
Date: Tue, 20 Jan 2009 14:12:20 +0100
From: Arnold Neumaier arnold.neuma...@univie.ac.at
To: Freek Wiedijk fr...@cs.kun.nl
Subject: The QED Project

Freek,

are there still activities related to the QED Project
 http://www-unix.mcs.anl.gov/qed/
I am contemplating writing a grant application for something going
in a similar direction, and would like to know about which people to
contact for possible collaboration.

What is your current assessment of what it takes to realize an
updated version of the QED project?


Best wishes,

Arnold

http://www.mat.univie.ac.at/~neum/


--
This SF.net email is sponsored by:
SourcForge Community
SourceForge wants to tell your story.
http://p.sf.net/sfu/sf-spreadtheword
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] System Announcement: ProofWeb

[Freek Wiedijk]

SYSTEM ANNOUNCEMENT: PROOFWEB

We are pleased to announce the availability of our ProofWeb
system for teaching logic and using proof assistants through
the web.  For details go to the ProofWeb home page at:


http://proofweb.cs.ru.nl/


Attached to this mail is the text on the ProofWeb home page.

Cezary Kaliszyk
Dan Synek
Femke van Raamsdonk
Freek Wiedijk
Herman Geuvers
James McKinna


WHAT IS PROOFWEB?

ProofWeb is both a system for teaching logic and for using
proof assistants through the web.

ProofWeb can be used in three ways.  First, one can use the
guest login, for which one does not even need to register.
Secondly, a user can be a student in a logic or proof
assistants course.  We are hosting courses free of charge.
If you are a teacher and would like to host your course on
this server, send email to [EMAIL PROTECTED]  Thirdly,
if teachers do not want to trust us with their students'
files, they can freely download the ProofWeb system and
run it on a server of their own.

LOGIC ON THE WEB

ProofWeb is a system for practising natural deduction on the
computer.  It is almost, but not quite, entirely unlike the
Jape system.  ProofWeb is based on the Coq proof assistant
and runs inside any modern web browser.  To use ProofWeb
one does not need to install software locally, not even a
plugin: a web browser is all one needs.  With ProofWeb one
runs logic exercises on a web server, just like gmail keeps
all mail messages on its server.  This means that students
will be able to access their exercises wherever they have
a web browser, and that teachers at any time can see the
status of their students' work.

ProofWeb comes with a database of basic logic exercises
that are graded according to difficulty.  The ProofWeb
system automatically grades the exercises of the students.
To the students this is presented as a traffic light:
their goal is to get a green light for all their exercises.

A ProofWeb user talks to the Coq system on the server
without any translation.  There just are a few additional
tactics to make Coq's behavior follow the logic textbooks.
This means that in ProofWeb the full power of Coq is
available, even to beginner students.  On the other hand
ProofWeb tries hard to present deductions exactly the way
they look in the textbooks.  In particular ProofWeb exactly
follows the conventions of a well-known logic textbook,
Logic in Computer Science: Modelling and Reasoning about
Systems by Michael Huth and Mark Ryan, published by
Cambridge University Press.  For this reason ProofWeb is
especially attractive for courses that use this textbook.
ProofWeb both supports Gentzen-style natural deduction in
which proofs look likes trees with the conclusion at the
root, and Fitch-style natural deduction in which proofs
consist of lines grouped together with boxes or flags.

PROOF ASSISTANTS ON THE WEB

ProofWeb is a system that allows anyone to try out proof
assistants without installing anything.  It is almost, but
not quite, entirely unlike the Proof General interface for
proof assistants.  ProofWeb was designed to be used with
Coq, but the interface has been successfully extended to
other proof assistants, and in particular it supports the
Isabelle system.

Although ProofWeb was designed for teaching logic to
undergraduate computer science students, it also has been
successfully used to teach proof assistant courses to
graduate students.

RELATED PROJECTS

The ProofWeb interface has been used and extended in various
projects.  The main ones are a prototype by Cezary Kaliszyk
and Pierre Corbineau of a system that combines ProofWeb
with a mathematical encyclopedia in the style of Wikipedia,
and PC-Extra, an arbitrary precision calculator by Cezary
Kaliszyk, based on the PhD work of Russell O'Connor.

ABOUT PROOFWEB

ProofWeb was developed in 2006 and 2007 in the education
innovation project Web deduction for education in formal
thinking which was financed by Surf Foundation, the Radboud
University Nijmegen and the Free University Amsterdam.
The main developer of the system was Cezary Kaliszyk, after
ideas by Freek Wiedijk.  The ProofWeb exercise database
and a first version of the natural deduction tactics were
developed by Maxim Hendriks.  ProofWeb was refined based
on experiences with the system in courses given by Femke
van Raamsdonk, Hanno Wupper and Roel de Vrijer.


-
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=100url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Second CFP - JAR special issue for PLMMS

[Freek Wiedijk]

Second CALL FOR PAPERS

Special issue on Programming Languages and Mechanized Mathematics Systems

   Journal of Automated Reasoning

[See HTML version at http://www.cas.mcmaster.ca/~carette/jplmms/cfp.html ]

Context

   This special issue is focused on the intersection of programming
   languages (PL) and mechanized mathematics systems (MMS). The latter
   category subsumes present-day computer algebra systems (CAS),
   interactive proof assistants (PA), and automated theorem provers (ATP),
   all heading towards fully integrated mechanized mathematical assistants
   that are expected to emerge eventually.

   The two subjects of PL and MMS meet in many interesting ways, in
   particular in the following main topics of this journal issue.

 * Dedicated input languages for MMS: covers all aspects of languages
   intended for the user to deploy or extend the system, both
   algorithmic and declarative ones. Typical examples are tactic
   definition languages such as Ltac in Coq, mathematical proof
   languages as in Mizar or Isar, or specialized programming languages
   built into CA systems. Of particular interest are the semantics of
   those languages, especially when current ones are untyped.
 * Mathematical modeling languages used for programming: covers the
   relation of logical descriptions vs. algorithmic content. For
   instance the logic of ACL2 extends a version of Lisp, that of Coq
   is close to Haskell, and some portions of HOL are similar to ML and
   Haskell, while Maple tries to do both simultaneously. Such
   mathematical languages offer rich specification capabilities, which
   are rarely available in regular programming languages. How can
   programming benefit from mathematical concepts, without limiting
   mathematics to the computational worldview?
 * Programming languages with mathematical specifications: covers
   advanced mathematical concepts in programming languages that
   improve the expressive power of functional specifications, type
   systems, module systems etc. Programming languages with dependent
   types are of particular interest here, as is intensionality vs
   extensionality.
 * Language elements for program verification: covers specific means
   built into a language to facilitate correctness proofs using MMS.
   For example, logical annotations within programs may be turned into
   verification conditions to be solved in a proof assistant
   eventually. How need MMS and PL to be improved to make this work
   conveniently and in a mathematically appealing way?

   These topics have been addressed in the PLMMS 2007
   http://www.cas.mcmaster.ca/plmms07/ and PLMMS 2008
   http://events.cs.bham.ac.uk/cicm08/workshops/plmms/ workshops
   (associated with Calculemus http://www.calculemus.net/). While the
   journal issue emerges from that community, submission is open to
   everyone interested in any of these topics!

Submission

   Manuscripts should not have been previously published in archival
   journals nor have been submitted to, or be in consideration for, any
   journal or conference. Significantly revised and enhanced papers
   published in workshop or conference proceedings are welcome. All
   submissions will be reviewed according to scholarly standards for
   scientific journal publications. See also the general JAR submission
   policies.

   We suggest a page limit of approximately 25 pages, using the LaTeX
   macros ftp://ftp.springer.de/pub/tex/latex/svjour3/global/
   provided by Springer. Instead of using the Springer online
   submission system, please submit papers in PDF through EasyChair
   http://www.easychair.org/conferences/?conf=jplmms2008

Important dates

 * Submission deadline: 10th November 2008.
 * Notification: January 16th 2009.
 * Final versions: March 30th 2009.

Editors of the special issue

 * Jacques Carette (McMaster University, Canada)
 * Makarius Wenzel (Technische Universitaet Muenchen, Germany)
 * Freek Wiedijk   (Radboud University Nijmegen, Netherlands)

-
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=100url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR)

[Freek Wiedijk]

CALL FOR PAPERS

Special issue on Programming Languages and Mechanized Mathematics Systems

Journal of Automated Reasoning

[See HTML version at http://www.cas.mcmaster.ca/~carette/jplmms/cfp.html ]

Context

   This special issue is focused on the intersection of programming
   languages (PL) and mechanized mathematics systems (MMS). The latter
   category subsumes present-day computer algebra systems (CAS),
   interactive proof assistants (PA), and automated theorem provers (ATP),
   all heading towards fully integrated mechanized mathematical assistants
   that are expected to emerge eventually.

   The two subjects of PL and MMS meet in many interesting ways, in
   particular in the following main topics of this journal issue.

 * Dedicated input languages for MMS: covers all aspects of languages
   intended for the user to deploy or extend the system, both
   algorithmic and declarative ones. Typical examples are tactic
   definition languages such as Ltac in Coq, mathematical proof
   languages as in Mizar or Isar, or specialized programming languages
   built into CA systems. Of particular interest are the semantics of
   those languages, especially when current ones are untyped.
 * Mathematical modeling languages used for programming: covers the
   relation of logical descriptions vs. algorithmic content. For
   instance the logic of ACL2 extends a version of Lisp, that of Coq
   is close to Haskell, and some portions of HOL are similar to ML and
   Haskell, while Maple tries to do both simultaneously. Such
   mathematical languages offer rich specification capabilities, which
   are rarely available in regular programming languages. How can
   programming benefit from mathematical concepts, without limiting
   mathematics to the computational worldview?
 * Programming languages with mathematical specifications: covers
   advanced mathematical concepts in programming languages that
   improve the expressive power of functional specifications, type
   systems, module systems etc. Programming languages with dependent
   types are of particular interest here, as is intensionality vs
   extensionality.
 * Language elements for program verification: covers specific means
   built into a language to facilitate correctness proofs using MMS.
   For example, logical annotations within programs may be turned into
   verification conditions to be solved in a proof assistant
   eventually. How need MMS and PL to be improved to make this work
   conveniently and in a mathematically appealing way?

   These topics have been addressed in the PLMMS 2007
   http://www.cas.mcmaster.ca/plmms07/ and PLMMS 2008
   http://events.cs.bham.ac.uk/cicm08/workshops/plmms/ workshops
   (associated with Calculemus http://www.calculemus.net/). While the
   journal issue emerges from that community, submission is open to
   everyone interested in any of these topics!

Submission

   Manuscripts should not have been previously published in archival
   journals nor have been submitted to, or be in consideration for, any
   journal or conference. Significantly revised and enhanced papers
   published in workshop or conference proceedings are welcome. All
   submissions will be reviewed according to scholarly standards for
   scientific journal publications. See also the general JAR submission
   policies.

   We suggest a page limit of approximately 25 pages, using the LaTeX
   macros ftp://ftp.springer.de/pub/tex/latex/svjour3/global.zip
   provided by Springer. Instead of using the Springer online
   submission system, please submit papers in PDF through EasyChair
   http://www.easychair.org/conferences/?conf=jplmms2008

Important dates

 * Submission deadline: 10th November 2008.
 * Notification: January 16th 2009.
 * Final versions: March 30th 2009.

Editors of the special issue

 * Jacques Carette (McMaster University, Canada)
 * Makarius Wenzel (Technische Universitaet Muenchen, Germany)
 * Freek Wiedijk   (Radboud University Nijmegen, Netherlands)

-
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=100url=/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info