GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → JBakouny → Scallina

JBakouny / Scallina

Licence: gpl-3.0
A Coq-based synthesis of Scala programs which are correct-by-construction

Programming Languages

scala
5932 projects

Labels

functional-programmingcoqsynthesisformal-methods

Projects that are alternatives of or similar to Scallina

Tool lists
Links to tools by subject
Stars: ✭ 270 (+315.38%)
Mutual labels:  synthesis, formal-methods
fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-70.77%)
Mutual labels:  coq, formal-methods
koika
A core language for rule-based hardware design 🦑
Stars: ✭ 103 (+58.46%)
Mutual labels:  coq, formal-methods
Practical Fm
A gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+318.46%)
Mutual labels:  coq, formal-methods
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-7.69%)
Mutual labels:  coq
Noexception
Java library for handling exceptions in concise, unified, and architecturally clean way.
Stars: ✭ 56 (-13.85%)
Mutual labels:  functional-programming
Affect
Algebraic effects for Ruby
Stars: ✭ 56 (-13.85%)
Mutual labels:  functional-programming
Modules
Modules in R
Stars: ✭ 54 (-16.92%)
Mutual labels:  functional-programming
Mgo
Purely functional genetic algorithms for multi-objective optimisation
Stars: ✭ 63 (-3.08%)
Mutual labels:  functional-programming
Parser Combinators From Scratch
Code that accompanies the series
Stars: ✭ 56 (-13.85%)
Mutual labels:  functional-programming
Racket Algebraic
Algebraic structures for untyped Racket
Stars: ✭ 60 (-7.69%)
Mutual labels:  functional-programming
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-12.31%)
Mutual labels:  coq
Heresy
A BASIC-flavored Lisp dialect
Stars: ✭ 60 (-7.69%)
Mutual labels:  functional-programming
Haskell Book Readers Exercises
Exercises from the readers of the Haskell Book
Stars: ✭ 56 (-13.85%)
Mutual labels:  functional-programming
Riscv Coq
RISC-V Specification in Coq
Stars: ✭ 63 (-3.08%)
Mutual labels:  coq
Jhc Components
JHC Haskell compiler split into reusable components
Stars: ✭ 55 (-15.38%)
Mutual labels:  functional-programming
Learning Sicp
MIT视频公开课《计算机程序的构造和解释》中文化项目及课程学习资料搜集。
Stars: ✭ 9,059 (+13836.92%)
Mutual labels:  functional-programming
Collapsing Towers
Collapsing Towers of Interpreters
Stars: ✭ 61 (-6.15%)
Mutual labels:  coq
Kari.hpp
Experimental library for currying in C++17
Stars: ✭ 58 (-10.77%)
Mutual labels:  functional-programming
Func
Functional additions to C
Stars: ✭ 58 (-10.77%)
Mutual labels:  functional-programming
View All Similar Projects ➔

Publications

A video demo is also available on YouTube.

Quick start guide

First, download the Scala Build Tool (SBT) from http://www.scala-sbt.org/download.html

Then, in the project's main directory run the command sbt assembly

Finally, the below command:

scala target/scala-2.12/scallina-assembly-<scallina-version>.jar <path-to-coq-source-file.v>

can be executed from the project's main directory in order to run Scallina.

Also, the below command should also work:

java -jar target/scala-2.12/scallina-assembly-<scallina-version>.jar <path-to-coq-source-file.v>

Usage Examples

Packaged examples are available under packaged-examples

Additional examples of Coq .v files that can be translated to Scala are available under src/test/resources/

Compiling the Generated Scala Files

The generated files can be compiled with the scalac Scala compiler provided that the Scallina Standard Library is included in the classpath.

For a practical example, see the compile-scala-code.sh script in packaged-examples/v0.7.0/SelectionSort.

The source code of the Scallina Standard Library is available under src/main/resources/scala/of/coq/lang.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].