coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactics that use Matlab

From: Adam Chlipala <adamc AT csail.mit.edu>
To: pfirodmoten AT gmail.com
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactics that use Matlab
Date: Tue, 30 Jul 2013 14:47:54 -0400

On 07/30/2013 02:00 PM,
pfirodmoten AT gmail.com
wrote:

Is it possible to create tactics in Coq that use Matlab or Octave?

Certainly. You can write arbitrary plugins in OCaml. Things are most interesting when you want to write such tactics in a way that doesn't require expanding Coq's trusted code base (i.e., proof checker), but I'm sure you could write many worthwhile proof-generating procedures that call out to Matlab.

[Coq-Club] Tactics that use Matlab, pfirodmoten, 07/30/2013
- Re: [Coq-Club] Tactics that use Matlab, Adam Chlipala, 07/30/2013
- Message not available
  - Re: [Coq-Club] Tactics that use Matlab, Kristopher Micinski, 07/30/2013