[Hol-info] MEMOCODE 2013 Call for Papers and Design Contest (EXTENDED DATES)

2013-05-07 Thread Marly Roncken
Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: CALL FOR PAPERS - MEMOCODE 2013 (NOTE: NEW EXTENDED DATES for PAPERS and DESIGN CONTEST) Eleventh ACM/IEEE International Conference on Formal Methods

[Hol-info] MEMOCODE Design Contest 2013 -- start May 15

2013-05-07 Thread Nurvitadhi, Eriko
Unsubscribe: https://lists.cs.columbia.edu/cucslists/listinfo/memocode Unsubscribe: Hi all, I would like to let you know that the MEMOCODE Design Contest for this year is coming up soon, on May 15. More details are available at http://memocode.

[Hol-info] FMCAD 2013 Final Call for Papers

2013-05-07 Thread Chao Yan
FMCAD 2013 - FORMAL METHODS IN COMPUTER-AIDED DESIGN FINAL CALL FOR PAPERS International Conference on Formal Methods in Computer-Aided Design http://www.fmcad.org/FMCAD13 Portland, OR, USA October 20-23, 2013 IMPORTANT DATES Abstract Submission: May 8 Paper Submission: May 15 Author Notificat

Re: [Hol-info] Learning HOL Light

2013-05-07 Thread Ramana Kumar
> > Do such regexp issues arise in HOL4 and SML? > HOL4 does not have a separate tactic language. Proof scripts are written in SML directly. (The SML implementation will have a parser etc. though.) HOL4 does have a sophisticated parser for the object language of HOL terms and types, which I thin

Re: [Hol-info] Learning HOL Light

2013-05-07 Thread Ramana Kumar
You can't detect matching braces with regular expressions. (See e.g. http://stackoverflow.com/questions/546433/regular-expression-to-match-outer-brackets .) What you probably need is to define your tactic language with a grammar and write a parser for it. You're going down a route that I think ma

Re: [Hol-info] Learning HOL Light

2013-05-07 Thread Bill Richter
Thanks, Ramana! I created my thmlist_tactics list in the same way that HOL Light creates the theorems database in hol_light/database.ml: needs "help.ml";; theorems := [ "ABSORPTION",ABSORPTION; "ABS_SIMP",ABS_SIMP; "ADD",ADD; [...] "vector",vector ];; That doesn't strike me as a painful solutio