Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Tom Ridge's Homepage
[go: Go Back, main page]
| Home | Consulting | Documents | Links | Work |

Tom Ridge's Homepage

This page is located at http://www.cl.cam.ac.uk/users/tjr22/index.html.

News

  • Model checking Michael's hazard pointers algorithm, prior to verifying a version running with weak memory. OCaml model-checking code is hazard.ml
  • A short script to figure out dependencies between HOL files, based on .HOLMK directory info. Could easily be modified to make a dot file to visualise theory dependencies in HOL (I did this a while ago, but lost the script files, so am gradually reconstructing them). File is deps.sh
  • 2008-02-13 My version of McCarthy's 91 function in Isabelle McCarthy.thy
  • 2008-02-12 A rigorous approach to networking: TCP, from implementation to protocol to service. ARG lunch talk ridge08tcp_service_arg_talk.pdf ridge08tcp_service_arg_talk.ps
  • 2008-02-08 A rigorous approach to networking: TCP, from implementation to protocol to service. Accepted to FM'08. ridge08stream_spec.pdf ridge08stream_spec.ps
  • 2008-02-06 Trying to build mosml on the new 64bit machine gives: 
    make[1]: Entering directory `/local/scratch/tjr22/dist/mosml/src/mosmllib'
../camlrunm ../mosmlcmp -stdlib ../mosmllib -P none -imptypes Array.sml
*** glibc detected *** ../camlrunm: munmap_chunk(): invalid pointer: 0x0000000000633000 ***
    The fix is described here.
  • 2008-01-09 The distributed persistent queue, written in OCaml, that I am currently working on is in directory queue2. I'm posting it here so interested people can get a feel for the type of thing I'm trying to verify currently.
  • 2008-01-09 I am working on a verification of a distributed persistent queue, written in OCaml. This requires a model of OCaml, hosts, networks, mutexes, condition variables and so on. I have a preliminary version of the semantics in OCaml, in directory operational. I'm pretty pleased with it so far.
  • 2007-11-19 I have a student doing a project on formalizing and implementing BASH. This has forced me to get to grips with BASH by reading the BASH reference. It was actually quite interesting, and I wish I'd done it a long time ago. BASH is a reasonable language, but with some major problems, and it's too complicated of course, but you can do a fair amount of higher-order functional programming. A trivial example of recursion is my implementation of factorial fact.sh
  • 2007-10-25 Another implementation of a CEK machine in OCaml, with minimal contexts and better use of types cek3.ml.
  • 2007-10-25 A little implementation of a CEK machine in OCaml is cev.ml (mis-named). Sufficiently fiddly that there are sure to be bugs in it!
  • 2007-10-04 To arrive where we started: experience of mechanizing binding. Workshop on Mechanizing Metatheory 2007, talk. wmmBindingTalk20071004.pdf wmmBindingTalk20071004.ps
  • 2007-08-16 I recently gave a talk where I suggested that working with a naive representation of binding (vars as strings) was a good approach. I have looked at previous proofs to see whether this approach is viable. An example is the following note. Strong Normalisation for STLC via representations. A truly elementary proof, not using properties of alpha. 2007-08-16 ridge07snrep.pdf ridge07snrep.ps
  • 2007-08-10 A recent talk about binding. If we forget about de Bruijn and HOAS, I believe we are best off working with a unquotiented raw term representation. Attempts to mechanize binding. Talk discussing some attempts to mechanize binding, and concluding that an unquotiented raw term approach is best. bindingTalk20070810.pdf bindingTalk20070810.ps
  • 2007-07-19 My whiteboard shows me trying to figure out how to prove that one alpha equivalence (the one in blue at the top) implies another (the one in blue at the bottom). Pretty!
  • A rigorous approach to networking: TCP, from implementation to protocol to service 2007-07-01 stream_spec.pdf stream_spec.ps Submitted to INFOCOM2007
  • To arrive where we started: experience of mechanizing binding. Accepted to Workshop on Mechanizing Metatheory 2007. 2007-06-18 ridge07wmm.pdf ridge07wmm.ps
  • My TPHOLs 2007 submission was accepted. The paper is ridge07tphols.pdf ridge07tphols.ps
  • 2007-05-16 An excerpt from my POPLmark proofs (which are still a work in progress). I am interested in feedback regarding the readability of these proofs, and how they compare to the informal versions. Comments welcome. transNarrowScript.sml
  • 2007-04-10 I am a listed author on the paper presenting Ott, a tool to support the task of writing program language definitions. My contribution was to do a few proofs on the Isabelle side, and to check the Isabelle definition generation. ott.pdf
  • 2007-03-19 Some new directions for program verification. Draft of a paper for TPHOLs 2007, talking about verification on top of operational semantics, and weak memory models. ridge07tphols.pdf ridge07tphols.ps
  • 2007-03-07 Slides for the Edinburgh talk tomorrow, on operational reasoning and weak memory models. edTalk20070308.pdf edTalk20070308.ps
  • 2007-02-20 A formal, mechanised proof of Peterson's mutual exclusion algorithm, for a weak memory model. Proofs, in Isabelle/HOL, in directory petersonWeak.
  • 2007-01-24 Slides for Hoare's concurrency meeting today. I presented the verification of an OCaml implementation of Peterson's algorithm. concTalk20070124.pdf concTalk20070124.ps
  • 2007-01-13 Our beautiful son Freddie was born at 12.17 this morning. A picture is here.
  • 2006-11-27 After more than a year of being frustrated with HOL indentation, I decided to write my own HOL indentation code. I have been put off by the thought of having to delve into xemacs indentation algorithms. However, I found an easy way to interface between xemacs and another program (found on a python mailing list somewhere), and then wrote some simple indentation code in ocaml. The code is extremely buggy... you have been warned! holtidy.ml
  • 2006-11-20 Just got back from ICNP06. Santa Barbara is really a very cool place. Presentation went well I think. The slides, which accompany the paper below, are at icnp06slides.pdf icnp06slides.ps
  • 2006-10-17 This has been around for a while, but I hadn't got round to posting it. A paper for ICNP2006 about formalising some specification/algorithm in HOL and extracting a testing oracle. Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL ridge06icnp.pdf ridge06icnp.ps Accepted for ICNP2006
  • 2006-09-30 POPLmark 1a challenge, formalising transitivity proofs for F-sub using a named interface layered on de Bruijn.
  • 2006-09-14 POPLmark 1a challenge, formalising transitivity proofs for F-sub using de Bruijn.
  • 2006-09-02 For comparison, a version of preservation for STLC using De Bruijn. stlc_db
  • 2006-09-01 Quite trivial, but preservation for STLC, based on the Isabelle output of Sewell's Ott tool. Of course, STLC requires handling variable capture and so on. I opted for my current favourite approach (a version of de Bruijn employing named abstraction). Quite slick! stlc_out.thy stlc_metatheory.thy
  • 2006-08-29 Trivial, but nice use of automation, and demonstrates Isabelle output of Sewell's new Ott tool, is the formalisation of progress and preservation for the cbv S.T.L.C
  • 2006-08-20 A problem with polymorphic variants: 
    let l = [`On;`Off];;

let j = List.filter (fun x -> match x with | `On -> false | `Off -> true);;
(* j can only produce lists of `Off, but this is not captured in the type *)

let rec k = fun x -> match x with
  | [] -> []
  | (x::xs) -> match x with 
      | `On -> k xs
      | `Off -> `Off :: k xs;;

(*        val k : [< `Off | `On ] list -> [> `Off ] list = <fun> *)
(* writing the function explicitly gives the required type info *)
    Presumably to determine the type of j in general would be undecidable. With a theorem prover, you would prove that j contained only Off s, so there is little point in using polymorphic variants to capture subtype properties like this.
  • 2006-08-07 Observational equivalence for STLC. Clearly, if we can observe normal forms, then observational equiv is the same thing as having identical normal forms. But observe that 
    (\ f :: alpha -> alpha. \ x :: alpha. f x) = (\ f \ x. f (f x))
    because 
    f
    must be the identity. So we really want (to be interesting) our notion of equivalence to be extensional. So introduce a ground type 
    bool
    with two distinct values and quotient by the obvious thing. Amazingly, this code of Dowek, based on this paper of Loader (based on ...) can enumerate the finite equivalence classes of terms at a particular type, and tell when two terms are obs. equiv.- for example, it identifies that the above two terms are obs. equiv.
  • 2006-08-05 Parametricity, Normal Forms for the Simply Typed Lambda Calculus. Shows how to prove e.g. that the only term of type alpha arrow alpha is the identity. stlcnf.pdf stlcnf.ps
  • 2006-08-02 Yet another implementation of the lambda calculus. This is my preferred concrete implementation for reasoning about (since alpha is the usual equality, but we have named abstraction), but because bound variables do not really have names, and so variables appear to alpha vary a lot when printing a term, a real named implementation is probably preferable where names of bound vars matter (which is quite often).nldb.ml
  • 2006-07-31 Strong Normalisation for the Simply Typed Lambda Calculus. Corrects some minor mistakes in a similar note by Rene David. 2006-07-31 (2007-08-16 Ott'ed) ridge06stlcsn.pdf ridge06stlcsn.ps
  • 2006-07-24 A Short Note on Informal Occurrence Notation. Discusses forall x. A[x] and A[t] notation. occNot.pdf occNot.ps
  • 2006-07-14 I encourage everyone to read the document of Rene David sn.ps on strong normalization for the simply typed lambda calculus. Beautiful in a different way to Tait/Girard reducibility candidates.
  • 2006-07-13 More HaMLet fixes. To get an interactive hamlet with mosml, make with-mosml as described below, then copy some files around. From unpacking hamlet.1.2.2.tar.gz, you have to do the following: 
    
touch Parser.grm.sig
touch Parser-sig.sml
touch Lexer.lex.sml
make clean
make with-mosml
cp smlnj-lib/*.u[io] .
cp fix/*.u[io] .
    You should now be able to run mosml, and load "Sml"; to load hamlet.
  • 2006-05-26 In my PhD, I suggested some new ways to extend automation and make it suitable for interactive use. At the time, I did not have completeness results. I believe I now have these, although they have not been mechanised. However, I have produced an implementation. I have extended my "verified prover" to deal with equality. I hope to extend this soon to deal with full first order terms. Then I hope to provide an implementation in HOL Light, or HOL. If you followed the "verified prover" paper, the code should be quite readable, and if you are familiar with completeness proofs, the correctness may even be clear. eqprover.ml
  • 2006-04-24 These are the steps I took to build HaMLet under mosml. 
    
The error message resembles the following:

make EXT=uo SYSTEM=mosml with-mosml-rec
make[1]: Entering directory `/local/scratch/tjr22/static/hamlet'
ml-yacc Parser.grm
ml-yacc: error   - line 1 of "Parser.grm", syntax error
(*                                                                              *)
^
make[1]: *** [Parser.grm.sig] Error 1
make[1]: Leaving directory `/local/scratch/tjr22/static/hamlet'
make: *** [with-mosml] Error 2

Unpack hamlet-1.2.2.tar.gz. Enter directory hamlet. Do not attempt to
make.  The file Parser.grm.sig is missing from the .tar.gz . The build
depends on Parser-sig.sml which depends on Parser.grm.sig . This means
that make will attempt to rebuild Parser.grm.sig using ml-yacc, which
will fail. The solution is to make a dummy Parser.grm.sig, then fool
make into believing that Parser-sig.sml is current.

touch Parser.grm.sig
touch Parser-sig.sml

However, there is a further problem. Lexer.lex.sml is older than the
other files (try ls --full-time). Thus make will attempt to rebuild
Lexer.lex.sml . Again, the solution is to fool make into believing
that Lexer.lex.sml is current.

touch Lexer.lex.sml

You should now be able to execute 

make with-mosml
  • 2006-04-12 Recently I've been looking at Ramsey's theorem, Kruskal etc. This prompted me to revisit my earlier proof of Ramsey and rework it considerably. The result is Ramsey.thy
  • 2006-03-02 MiniML Type Soundness Formalised and Mechanised in Isabelle/HOL miniml.pdf miniml.ps
  • 2006-02-19 A little exercise for Discrete Maths II, some simple transitive closure lemmas. This has been done so many times, but still worth doing for oneself. Isabelle/HOL theory file TransC.thy
  • 2006-01-12 My Research, submitted for a Wolfson fellowship application wolfson.ps
  • 2006-01-12 Peterson's algorithm in Isabelle/HOL peterson.pdf peterson.ps It is my intention to write a compendium study of three mutual exclusion algorithms that I have recently verified, Peterson's algorithm, Simpson's four slot algorithm, and Harris' three slot algorithm.
  • 2005-12-23 Another proof of the mutual exclusion property of Simpson's algorithm, this time using invariants. This proof is interesting for several reasons. Firstly, the invariant is the weakest possible invariant. It is also extremely syntactically simple, and therefore easy to understand. Furthermore, the proof of invariance of our strengthened mutual exclusion property involves nothing more powerful than simplification. Simpson5.thy
  • 2005-12-14 A little exercise, Simpson's four slot algorithm formalised and mechanised in Isabelle/HOL. Simpson.thy
  • 2005-12-14 RA Day talk "NETSEM: TCP/IP Formalised" 2005-12-14 raDayTalk20051214.pdf raDayTalk20051214.ps
  • 2005-12-06 Recently we have been pondering what it would take to formalise a MiniML style evaluator in HOL, with a view to writing some simple network programs over the top of it (in the style of Michael Compton's work, but with a more substantial/generic MiniML evaluator). I hacked up a miniml.ml interpreter in OCaml based on Pfenning's computation and deduction notes, which seems to work pretty well (although I have to admit I haven't convinced myself about the evaluation of fix!). Now to include access to state etc.
  • 2005-12-01 Peterson's mutual exclusion algorithm for 2 processes formalised and mechanised in Isabelle/HOL Peterson.thy
  • 2005-11-10 DRAFT Craig's Interpolation Theorem, formalised and mechanised in Isabelle/HOL craig.ps
  • 2005-11-08 Craig's Interpolation Theorem. Slides for the ARG lunch talk 2005-11-09 argTalk20051109.pdf argTalk20051109.ps
  • 2005-10-28 Craig's interpolation theorem formalised and mechanised in Isabelle/HOL. The directory is cutElim, or grab the whole lot as cutElim.tar.gz.
  • 2005-09-15 Apparently the example below is not a soundness bug, because there are "hidden" assumptions, which are not expressible in the language of HOL currently, although they are tracked by Isabelle/HOL.
  • 2005-09-14 Possible soundness bug in Isabelle 
    theory False = Main:

axclass blurg < type
  blurg: "! x. x ~= x"

lemma l: "(x ~= (x::'a::blurg)) ==> False"
  apply(simp)
  done

lemma "False"
  apply(rule l[of "x"])
  apply(simp only: blurg)
  apply(simp)
  done

end
  • 2005-09-07 Amusing? Here is the definition of alpha equivalence for HOL terms extended with type quantification.Pi is my type binder. So
    Pi A. \ x:A. x = x
    is alpha equiv to
    Pi B. \ y:B. y = y 
    
(* ------------------------------------------------------------------------- *)
(* Tests for alpha-convertibility (equality ignoring names in abstractions). *)
(* ------------------------------------------------------------------------- *)

  let newvar = variant

  let rec newtyvar avoid ty =
    let s = dest_vartype ty in
    let s' = s ^ "'" in
    if mem ty avoid then newtyvar avoid (mk_vartype s')
    else ty

  let rec paconv ftyvs fvs (vsub:term->term) tyvsub t (vsub':term->term) tyvsub' t' = match (t,t') with
    Var(x,ty), Var(x',ty') ->
      let ty = type_subst' tyvsub ty in
      let ty' = type_subst' tyvsub' ty' in
    (vsub (Var(x,ty))) = (vsub' (Var(x',ty')))
    | Const(s,ty), Const(s',t') -> (s,type_subst' tyvsub ty) = (s', type_subst' tyvsub' t')
    | Comb(s1,t1),Comb(s2,t2) ->
    paconv ftyvs fvs vsub tyvsub s1 vsub' tyvsub' s2
    & paconv ftyvs fvs vsub tyvsub t1 vsub' tyvsub' t2
    | Abs(Var(x,ty),t),Abs(Var(x',ty'),t') ->
    let (ty,ty') = (type_subst' tyvsub ty, type_subst' tyvsub' ty') in
      if ty = ty' then
        let (y:term) = newvar fvs (Var(x,ty)) in
        let vsub = fun v -> if v = Var(x,ty) then y else vsub v in
        let vsub' = fun v' -> if v' = Var(x',ty') then y else vsub' v' in
          paconv ftyvs (y::fvs) vsub tyvsub t vsub' tyvsub' t'
      else
        false
    | Pi(ty,t), Pi(ty',t') ->
    let y = newtyvar ftyvs ty in
    let tyvsub = fun t -> if t = ty then y else tyvsub t in
    let tyvsub' = fun t' -> if t' = ty' then y else tyvsub' t' in
      paconv (y::ftyvs) fvs vsub tyvsub t vsub' tyvsub' t'
    | _ -> false

  let aconv tm1 tm2 = Pervasives.compare tm1 tm2 = 0
  or (let ftyvs = union (type_vars_in_term tm1) (type_vars_in_term tm2) in
      let fvs = union (frees tm1) (frees tm2) in
    paconv ftyvs fvs I I tm1 I I tm2)
  • 2005-09-01 Work on the stream spec for the NETSEM project continues apace. I hope to have most of the stream spec done by tomorrow end, and then we concentrate on getting the trace generation and testing architecture up and running for two hosts communicating over a lossy duplicating and out of order network.
  • 2005-08-09 TPHOLs 2005. Latest version of the verified prover. Directory is prover, tar.gz is prover.tar.gz. TPHOLs doc preprint (bad affiliations, spelling mistake towards end) is prover.pdf.
  • 2005-07-06 I have recently arrived in Cambridge and for the last month I have been working on the Netsem project. This is a project which aims to formalise TCP. TCP is based on a sliding window protocol. Surprisingly, all the existant proofs concerning the correctness of sliding window protocols are deficient in various ways, that is, they fail to address realistic sliding window protocols. In particular, the correctness of many sliding window protocols is based crucially on the maximum time a packet can remain in the network without being delivered or lost, but this usually does not appear in the proofs. I have written a paper proof which purports to show that the segment number at which wraparound occurs (MAXSEG) must be greater that 2*WIN + MSL, where WIN is the sender and receiver window length, and MSL is such that MSL*delta is a bound on the maximum time a packet can remain in the network. delta is the time it takes a sender to send one packet of data. Thus, given a bound on the bytes that can be sent in a packet, one has a relation between MSL, WIN and sender capacity. I am currently formalising this proof in Isabelle and HOL, although modular arithmetic (segments are numbered modulo MAXSEG) is a real pain.
  • 2005-04-27 Type Quantification, Abstract Algebra and Predicate Subtyping. Part of my thesis concerns theory interpretation. In the following note I give an example of using type quantification to alleviate a common problem involved in formalising abstract algebra in a type system. The problem is that one wants to work with a mathematical structure, say groups, sometimes considering the carrier to be the whole type, and sometimes considering the carrier to be a subset of the type. typeQuantification.pdf typeQuantification.ps
  • 2005-04-08 The following appeared on the FOM email list on the 5th
    For any n, it is possible to enumerate all the n-tuples. I have seen formulas that for any x, will give the x-th member of an enumeration of pairs. I am wondering, however, whether anyone knows of a definition of a function that will take any three numbers, x y and z, and yield the z-th member of the y-th x-tuple in an enumeration of the x-tuples. Presumably, such a function is definable within Robinson's Arithmetic, since there is an effective procedure for computing such a function. It is not obvious to me, however, whether there is some natural way of defining such a function. Paul Studtmann
    Happily, I had already done just that. My reply to Paul was:
    Just take the y-th x-tuple and project onto the z coordinate. For instance, there is a draft at http://homepages.inf.ed.ac.uk/s0128214/doc/enum.pdf where I define a function (in higher order logic, mechanised in Isabelle/HOL theorem prover) called listDiag which takes an x and a y and returns the y-th x-tuple (represented as a list). From here, one would just take the z-th element of the tuple. This is all definable in primitive recursive arithmetic I think. The trick is to use diag recursively. Hope this answers your question. Yours sincerely Tom
  • 2005-03-23 The news is that there will be no more news till my PhD is finished. I got a job at Cambridge Computer Laboratory working with Peter Sewell et al. on the NETSEM project. Now I really must write up.
  • 2005-03-08 A minor variation of my verified theorem prover in OCaML, this time supporting negation and implication directly, rather than as defined notions. The system is Schwichtenberg's G3c g3c.ml
  • 2005-02-14 DRAFT A Mechanically Verified, Efficient, Sound and Complete Theorem Prover for First Order Logic. Discusses my recent mechanisation of soundness and completeness proofs for first order logic following Wainer and Wallen. prover.pdf prover.ps
  • 2005-02-11 VERY DRAFT Efficiently Enumerating Terms. Discusses how to enumerate first order terms without repetition. enum.pdf enum.ps
  • 2005-02-10 For a long time I have been interested in trying to make tableaux competitive with resolution. For various reasons, I favour a simple approach to tableaux, which eschews unification in favour of simply enumerating witness terms to instantiate forall L, exists R. The barrier to this was to come up with an efficient (tail recursive) function that enumerates all terms that can be formed from a given set of term constructors. For example, if we have a constant c, a unary function f, and a binary function g, then we seek an enumeration c, f(c), g(c,c), f(f(c)), g(c,f(c)) ... Whilst browsing the web for "term enumeration", I came across some work by Berghofer, that makes the point that the simple diag function, which enumerates pairs of natural numbers, suffices for most applications. I was then able to implement a tail recursive enumeration of terms. Example output is enumOutput.txt. I plan to integrate this with my tableaux prover and then see whether it is competitive with resolution provers for predicate logic problems (without equality). Watch this space!

  • 2005-02-01 I have verified an implementation of the lambda calculus using named variables in Isabelle/HOL. I tackle alpha conversion, the Barendregt variable convention and substitution. I then transport the definitions to OCaML to get 3 functions, one for each of these operations. The functions are admirably concise, efficient, and hopefully clearly correct, without recourse to the formalisation. The function definitions are namedLambda.ps. namedLambda.ml

    UPDATED 2005-02-04 I have carried out essentially the same verification for the following algorithms based on two separate namespaces for parameters and vars. These algorithms are valid on wellformed terms, i.e. terms with no free Vars. This verification was substantially easier than the previous one which used only named vars, and the intuitive content is also clearer. To sum up: this is probably the correct representation of lambda terms, but in implementations (of e.g. theorem provers) one should restrict the term forming operations to some small routines, to ensure that only wellformed terms are being manipulated (i.e. no malformed terms can be created). I can't quite decide whether I like this version because the intuitive content is clearer, or the other version with just a single namespace, and the advantage that the term forming routines do not have to be part of the kernel. namedLambda2.ml

  • 2005-01-22 DRAFT Proof Terms: Theory, Implementation and Transformation. Discusses implementing proof terms in HOL Light, with short notes on proof transformation. seqpftms.pdf seqpftms.ps
  • 2005-01-21 A new formalised development of Simulation Relations, mechanised in Isabelle/HOL, which has advantages over previous versions in that definitions have been tightened, modularity improved and proofs hopefully more comprehensible (and certainly shorter). SimpleSimulationRelation.thy. Also requires Kripke.thy
  • 2005-01-19 Second PhD document discusses liveness reasoning for Stenning's Protocol, mechanised in Isabelle/HOL. The draft is liveness.pdf liveness.ps.
  • 2005-01-19 In order to make my PhD more modular and manageable, I will be putting selfcontained parts up on the web. The first discusses simulation relations in Isabelle/HOL. The draft is simulationRelation.pdf simulationRelation.ps. This also allows me to reference these extended versions from an overview paper I am currently working on.
  • 2005-01-10 Following on from Laura's recent Dream talk about verifying a convex hull algorithm, I thought I'd have a shot. Presumably the algorithm is already known, but perhaps the proof of correctness is not. The code is hull_alg.ml. The drafts are convexHull.pdf convexHull.ps.
  • 2004-12-26 Building on work with proof terms, I have been looking at a module system for HOL based systems. The idea is to build on the underlying module systems present in OCaml, SML etc. Category theory represents a ferocious target for formalisation. To this end, I have mocked up a dummy implementation of categories using the OCaml module system. The file is mod3.ml. Over the next week or so I hope to reimplement this in HOL Light.
  • 2004-12-13 Over the last few days I have gutted the core of HOL Light, implemented my own axiom system, and implemented my own version of sequent/ natural deduction proof terms (with the benefits of both approaches). It takes about 5 minutes to print out the proofs of some very simple theorems. It is largely backwards compatible, but there seems to be some issues in simp.ml to deal with.
  • 2004-12-07 I tidied up some of the defns for my verified prover, and found that there was a roughly 200 percent increase in speed! This makes it feasible to execute the prover inside Isabelle on real examples. The directory is here, or you can download the whole thing as Verified-Prover.tar.gz.
  • 2004-11-29 During the Dream talk recently, people were pondering the deficiencies of HOL implementations in terms of context handling. I briefly wondered how easy it would be to implement a new version of HOL. This evening I sat down and had a first go at it. The file is lighter.ml. The axioms I am using are the top diagram of holRules.ps. I managed to derive T, but then realised I was going to need general beta conversion (i.e. not only at top level) for conj, which is slightly more complicated. Might be quite fun to do a quick port of equal.ml in HOL Light to this new setting.
  • 2004-10-23 Very rough draft of a description of my work on sequent level proof terms for HOL Light, including some stuff about rewriting proof terms using higher order rewriting. SUPERSEDED
  • 2004-10-23 Short piece about how one might come up with a proof of Godel's Incompleteness Theorem, in the style of Gower's articles about how to prove things. godelIncompleteness.pdf
  • 2004-09-27 I have produced a mechanically verified, efficient, sound and complete theorem prover for first order logic. The directory is here, or you can download the whole thing as Verified-Prover.tar.gz. Also contributed to the Archive for formal proofs. Responses from others:

    Many, many thanks for this contribution! -- Larry Paulson

    A very impressive piece of work! -- John Harrison

  • 2004-09-22 As indicated below, I have been playing around with proof terms. Here is a big proof.
  • 2004-09-20 I have implemented sequent level (i.e. replayable at the tactic level: important for proof planning etc.) proof terms for HOL Light, and implemented proof term transformation by higher order rewriting. Hopefully more to follow... but some of the files are here. SUPERSEDED
  • 2004-09-13 I have mechanised Ramsey's theorem (infinitary version) in Isabelle, as found in Boolos and Jeffrey "Computability and Logic" (with some minor improvements to the proof). The theory file is Ramsey.thy. (2004-09-20) Also available at the Archive for formal proofs
  • 2004-09-02 (updated 2004-09-20) I have made a first stab at transferring James Margetson's mechanisation of a completeness proof for FOL (conducted in HOL) to the current version of Isabelle. There is a tar.gz file, or you can browse the directory.
  • Documents section
  • New homepage. Not much here yet. I'll try and move some of the stuff over from the previous webpage bit by bit.

Keywords

This section just here to ensure web crawlers can do their job.

mechanise mechanize Isabelle Isabelle/HOL HOL HOL Light formalise formalize proof terms sequent first order logic higher order logic simulation relations state transition systems soundness completeness verify verification


Valid XHTML 1.0! Generated from xml source on Sun Mar 09 19:35:00 GMT 2008

You don't need all this machinery to write programs that might work. -- John Reynolds