Questions tagged [software-application]
Questions asking about software for Proof Assistants. Note: may not be app.
3
questions
1
vote
1
answer
39
views
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 ...
1
vote
1
answer
116
views
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 ...
10
votes
1
answer
79
views
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 ...
- 1,439