The Ivory EDSL
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
ivory-artifact hackage: update versions. Dec 16, 2016
ivory-backend-acl2 @ fa6667b hackage: update versions. Dec 16, 2016
ivory-backend-c Bump versions affected by GHC 8.4 compat changes Jul 13, 2018
ivory-eval hackage: update versions. Dec 16, 2016
ivory-examples compat shim for 7.10 Apr 18, 2017
ivory-formal-model Added pdf for isabelle theories Jul 22, 2014
ivory-hw Bump versions affected by GHC 8.4 compat changes Jul 13, 2018
ivory-model-check Build with GHC 8.2.2 and 8.4.3 Jul 11, 2018
ivory-opts Bump versions affected by GHC 8.4 compat changes Jul 13, 2018
ivory-paper Trevor's Haskell Symposium slides Jun 21, 2017
ivory-quickcheck hackage: update versions. Dec 16, 2016
ivory-serialize hackage: update versions. Dec 16, 2016
ivory-stdlib hackage: update versions. Dec 16, 2016
ivory Bump versions affected by GHC 8.4 compat changes Jul 13, 2018
.gitignore Compatibility fixes for template-haskell-2.12 and mainland-pretty-0.6 Aug 9, 2017
.gitmodules submodules: https rather than ssh (for public access). Nov 4, 2014
.travis.yml Point travis 7.10 build to correct stack.yaml file Jul 24, 2018
CODE_OF_CONDUCT.md add code of conduct Dec 14, 2015
LICENSE update README and add LICENSE file May 2, 2013
Makefile add --install-ghc to appease travis Apr 18, 2017
README.md Update README.md May 26, 2017
hackage.sh hackage script. Dec 16, 2016
stack-7.10.yaml add back stack-7.10 Aug 10, 2017
stack-8.0.2.yaml stack: add extra-deps Aug 10, 2017
stack-8.2.2.yaml Build with GHC 8.2.2 and 8.4.3 Jul 11, 2018
stack-8.4.3.yaml Build with GHC 8.2.2 and 8.4.3 Jul 11, 2018
stack.mk add --install-ghc to appease travis Apr 18, 2017
stack.yaml stack: add extra-deps Aug 10, 2017

README.md

Build Status

Ivory

Ivory is an embedded domain specific language (EDSL) which aims to provide a systems-level programming language that removes some common pitfalls of programming in C, without sacrificing expressivity.

This repository includes a user guide and some examples Ivory programs. More information and tutorials are available on ivorylang.org.

The following paper describes the Ivory language:

  • Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, Jamey Sharp, Eric Seidel, John Launchbury. Guilt-free Ivory. Haskell Symposium, 2015.

Please cite this paper for when citing the language.

Contents

  • ivory: the Ivory language implementation and interpreter
  • ivory-backend-c: a backend for compiling Ivory programs to C
  • ivory-examples: sample Ivory programs
  • ivory-opts: an optimization framework and some optimization implementations, for the Ivory AST.
  • ivory-bitdata: a macro language library for specifying bit-precise Ivory operations.
  • ivory-hw: a macro language library for writing hardware drivers in Ivory.
  • ivory-model-check: a backend for verifying Ivory programs with CVC4

Installing

Ivory is written in Haskell and uses several recent GHC extensions. It is known to work with with GHC 7.8.* and above.

We currently recommend using the Stack build tool for Ivory language packages and any programs which use them.

Copyright and license

Copyright 2013-2015 Galois, Inc.

Licensed under the BSD 3-Clause License; you may not use this work except in compliance with the License. A copy of the License is included in the LICENSE file.

Contributing

This project adheres to the Contributor Covenant code of conduct. By participating, you are expected to uphold this code. Please report unacceptable behavior to smaccm@galois.com.