anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-15 01:52:11 +03:00
Code Issues Projects Releases Wiki Activity
Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.
289 Commits 53 Branches 39 Tags 21 MiB
Haskell 81.8%
Agda 7.4%
Nix 3.7%
Common Lisp 3.5%
Idris 1%
Other 2.5%
8760f73d38
Go to file
Jan Mas Rovira 8760f73d38 [parser] allow '-' as the first character of an identifier. Use try for literals
2022-03-16 12:39:50 +01:00
.github/workflows fix compilation errors 2021-12-23 11:19:46 +01:00
agda-proofs [proofs] add some proofs on small matrices 2022-02-28 18:31:31 +01:00
app [app] add minihaskell command 2022-03-15 18:01:28 +01:00
assets add integer and string literals 2022-03-15 12:37:33 +01:00
docs Revisions on Frid. 17 Dec 2021-12-17 12:33:02 +00:00
examples [stdlib] add MiniJuvix standard library as a submodule 2022-02-03 18:06:59 +01:00
minijuvix-stdlib@ad8392f76e [stdlib] update 2022-02-28 18:24:52 +01:00
notes [scoper] Implement qualified names, open and import statements 2022-02-03 10:25:38 +01:00
src/MiniJuvix [parser] allow '-' as the first character of an identifier. Use try for literals 2022-03-16 12:39:50 +01:00
test add integer and string literals 2022-03-15 12:37:33 +01:00
tests add integer and string literals 2022-03-15 12:37:33 +01:00
.gitignore delete and ignore .ghci 2021-12-28 17:20:36 +01:00
.gitmodules [pretty] improve prettyprinter. Add proper parentheses handling 2022-02-04 00:09:00 +01:00
.hlint.yaml [ Makefile ] fixies for make prepare-push target 2021-12-30 09:56:58 -05:00
CHANGELOG.md First commit, initial project template. 2021-09-26 18:59:51 +02:00
hie.yaml [tests] setup basic testing 2022-02-15 14:12:53 +01:00
LICENSE First commit, initial project template. 2021-09-26 18:59:51 +02:00
Makefile [ Makefile ] fixies for make prepare-push target 2021-12-30 09:56:58 -05:00
minijuvix.agda-lib WIP. Adapting source code from heliaxdev/juvix for parsing purposes. 2021-11-11 20:08:49 +01:00
package.yaml [extensions] add TemplateHaskell and DeriveGeneric 2022-03-09 14:33:36 +01:00
README.md [ README ] fixed broken links 2021-12-30 10:53:36 -05:00
stack.yaml [stack] update resolver 2022-02-28 18:28:09 +01:00

README.md

MiniJuvix GPL-3.0-only license Haskell CI

This repository aims to be a conservative Haskell project of a tiny language with dependent types based on the Juvix project. The primary purpose is to be a laboratory to study/experiment in implementing a functional language with dependent types.

In this branch qtt, MiniJuvix aims to be programming language based on Quantitative type theory. Some Haskell code has been generated automatically by agda2hs. In the future, we want to prove properties about the Minijuvix programs directly in Agda.

The following is a tentative project structure, but it can change at any moment. See below the file project structure. The diagram shows the design of the compiler related with the project structure.

In the picture, syntax transformations are denoted by pᵢ and checking operations are denoted by cᵢ .