1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
# This CITATION.cff file was generated with cffinit.
# Visit https://bit.ly/cffinit to generate yours today!
cff-version: 1.2.0
title: Coq SimpleIO
message: 'If you use this software, please cite it as below.'
type: software
authors:
- given-names: Li-yao
family-names: Xia
email: xialiyao@cis.upenn.edu
affiliation: University of Pennsylvania
orcid: 'https://orcid.org/0000-0003-2673-4400'
- given-names: Yishuai
family-names: Li
email: yishuai@cis.upenn.edu
affiliation: University of Pennsylvania
orcid: 'https://orcid.org/0000-0002-5728-5903'
repository-code: 'https://github.com/Lysxia/coq-simple-io'
abstract: >-
This library provides tools to implement IO
programs directly in Coq, in a similar style to
Haskell. Facilities for formal verification are not
included.
IO is defined as a parameter with a purely
functional interface in Coq, to be extracted to
OCaml. Some wrappers for the basic types and
functions in the OCaml Pervasives module are
provided, and users are free to define their own
APIs on top of this IO type.
license: MIT
|
