SerAPI: Machine-Friendly, Data-Centric Serialization for COQ
Gallego Arias, Emilio Jesús
HAL, hal-01384408 / Harvested from HAL
We present SerAPI, a library and protocol for machine-friendly communication with the COQ proof assistant. SerAPI is implemented using Ocaml's PPX pre-processing technology, and it is specifically targeted to reduce implementation burden for tools such as Integrated Development Environments or code analyzers. SerAPI tries to address common problems that tools interacting with COQ face, providing a uniform and data-centric way to access term representations, proof state, and an extended protocol for document building. SerAPI is work in progress but fully functional. It has been adopted by the jsCoq and PeaCoq Integrated Development Environments , and supports running inside a web browser instance. For the near future, we are focused on extending the document protocol and providing advanced display abilities to clients.
Publié le : 2016-10-19
Classification:  theorem prover implementation,  program verification,  serialization,  interactive protocols,  user interfaces,  [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC],  [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL],  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO]Computer Science [cs],  [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]
@article{hal-01384408,
     author = {Gallego Arias, Emilio Jes\'us},
     title = {SerAPI: Machine-Friendly, Data-Centric Serialization for COQ},
     journal = {HAL},
     volume = {2016},
     number = {0},
     year = {2016},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-01384408}
}
Gallego Arias, Emilio Jesús. SerAPI: Machine-Friendly, Data-Centric Serialization for COQ. HAL, Tome 2016 (2016) no. 0, . http://gdmltest.u-ga.fr/item/hal-01384408/