Questions tagged [software-application]

Questions asking about software for Proof Assistants. Note: may not be app.

Filter by
Sorted by
Tagged with
1 vote
1 answer

Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?

The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows. For example, if an arrow is two-headed I need in Coq locally to ...
D Left Adjoint to U's user avatar
1 vote
1 answer

Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
D Left Adjoint to U's user avatar
10 votes
1 answer

Reasoning with the definition of Standard ML

I know that the definition of Standard ML has been mechanized in Twelf, but are there tools which allow me to verify my Standard ML code satisfies certain properties or specifications? I'm vaguely ...
Alex Nelson's user avatar
  • 1,439