Questions tagged [software-application]
Questions asking about software for Proof Assistants. Note: may not be app.
3
questions
1
vote
1
answer
84
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 ...
2
votes
1
answer
153
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
98
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,574