We are pleased to announce the call for proposals for hosting and
organising FroCoS-ITP-TABLEAUX 2025, on their 15th, 16th and 33rd
editions, respectively.
- FroCoS (http://frocos.cs.uiowa.edu/) is the main international event
for research on the development of techniques and methods for the
Hi all,
This year's CakeML Developers Meeting will be held 13-14 May 2019 at
Chalmers in Gothenburg Sweden. This meeting brings together developers
and users of CakeML -- anyone with an interest in CakeML is welcome.
The preliminary programme for the meeting is here:
://people.kth.se/~dbro/
- Associate Professor Magnus Myreen at Chalmers, Sweden
http://www.cse.chalmers.se/~myreen/
At KTH, this project will use the Coq proof assistant to design and
develop a verified model-checker and a synthesis mechanism that
correctly extracts an executable timed intermediate form
Certified Programs and Proofs (CPP) is an international forum on
theoretical and practical topics in all areas, including computer
science, mathematics, and education, that consider certification as an
essential paradigm for their work. Certification here means formal,
mechanized verification of
Certified Programs and Proofs (CPP) is an international forum on
theoretical and practical topics in all areas, including computer
science, mathematics, and education, that consider certification as an
essential paradigm for their work. Certification here means formal,
mechanized verification of
naming convention
> (e.g., those starting with an underscore or something like that) and
> then did the usual
> search (which can be on name fragment or pattern).
>
> Konrad.
>
>
> On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen <myr...@chalmers.se> wr
pe
> might be easiest for users to understand, so perhaps I can build that as well
> as term lists.
>
> Michael
>
> On 11/1/18, 11:08, "Magnus Myreen" <myr...@chalmers.se> wrote:
>
> Hi Michael,
>
> I see that you are considering to add a
Hi Michael,
I see that you are considering to add a TermSetData feature. Could you
please add something more general? I'd appreciate a feature that can
store the CakeML translator's state in theories. Currently, the CakeML
translator stores its state in a single theorem so that the other
theories
Hi all,
I'm looking to hire two new PhD students to work on interactive
theorem proving and functional programming, more precisely: on
CakeML-related topics (https://cakeml.org/) in HOL4
(https://hol-theorem-prover.org/). Kindly pass this on to
potential applicants.
* Application deadline: 25
On 27 January 2017 at 09:12, Thomas Tuerk <tho...@tuerk-brechen.de> wrote:
> Hello,
>
> many thanks. That does the trick and is much nicer than my hack.
>
> @Magnus Myreen: Do you think this is worth adding to the HOL Interaction
> manual?
Definitely! I've updated th
For some reason, the prefix C-u C-u to M-h M-r never seems to work for
me. I'm using Emacs 24.5 (the latest version) and have an up-to-date
HOL version.
My solution is to manually toggle quietness with M-h C-q. In other
words, to avoid output I press M-h C-q then M-h M-r then M-h C-q.
Cheers,
Hi hol-info,
Quick question: is there a tactic for instantiating a nested
existential based on a name? Example: for a goal such as
?x y z. ... y ...
I want to use a tactic foo_tac `y` `5` and get:
?x z. ... 5 ...
Is there such a foo_tac tactic? I suspect this functionality is there
Hi Masoume,
Have you tried RES_TAC? I think RES_TAC should get you ∀n. n ≤ C' ⇒ n
≠ w as an assumption.
Cheers,
Magnus
On 13 May 2014 09:01, masoume tajvidi mas.tajv...@gmail.com wrote:
Hi ,
I have a subgoal like this:
F
0. (winner' =
Hi Ian,
You should be able to find it under:
HOL/tools/hol-mode.{el,sml}
A while back, I wrote an 8-page guide to HOL and Michael Norrish' hol-mode:
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf
Regards,
Magnus
On 5 February 2012 17:26, Ian Zimmerman i...@buug.org wrote:
The
Hi Lu,
Both of your goals can be solved with:
SIMP_TAC std_ss [ALIGNED_INTRO,ALIGNED_CLAUSES]
See HOL/examples/machine-code/hoare-triple/addressScript.sml.
ALIGNED is another useful theorem about alignment, e.g.
REWRITE_CONV [ALIGNED] ``ALIGNED (a + 12w)``;
val it =
|- ALIGNED (a +
Hi,
Is it possible to define the following datatype in HOL4?
exp =
Var of num
| App of exp # exp
| Abs of (num - exp)
When the above is given to HOL_datatype, it responds:
Can't find definition for nested type: fun
(This datatype comes from Adam Chlipala's Coq paper at POPL'10.)
Hi Lu,
I saw that Thomas already provided a solution. Here's another simpler
proof of your example goal:
val th = prove(
``!p1 p2. PEQ p1 p2 == PEQ p2 p3 == PEQ p1 p3``,
SIMP_TAC std_ss [PEW_cases,FORALL_PROD])
where PEW_cases came from:
val (PEQ_rules, PEQ_ind, PEW_cases) = Hol_reln `
17 matches
Mail list logo
