CITATION.cff

# 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