Skip to content

Instantly share code, notes, and snippets.

Avatar

Marty Stumpf thealmarty

View GitHub Profile
@thealmarty
thealmarty / insertion_sort.cpp
Created Feb 13, 2021
Insertion sort in C++
View insertion_sort.cpp
#include <iostream>
#include <vector>
void insertion_sort(std::vector<int> & v) {
// invariant: the first i elements of v are sorted
for(size_t i = 1; i < v.size(); ++i) {
int value = v[i];
size_t j = i-1;
// invariant: elements of v from j+1 to i inclusive are sorted and >= value
for(; j >= 0 && v[j] > value; --j) {
View insertion_sort.c
#include <stdio.h>
void insertion(int v[], int size) {
// invariant: the elements of v before index i are sorted
for(int i = 1; i < size; ++i) {
int value = v[i];
int j = i;
// invariant: the elements of v between j and i are sorted and > value
for(;j > 0 && v[j-1] > value; --j) {
v[j] = v[j-1];
@thealmarty
thealmarty / Markdium-idris.idr
Created Dec 31, 2020
Markdium-Dependent types: formal definition and examples
View Markdium-idris.idr
onePlusOne : 1+1=2
onePlusOne = Refl
@thealmarty
thealmarty / UnificationImplementationPlan.md
Last active Sep 30, 2020
Unification implementation plan.
View UnificationImplementationPlan.md

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.

@thealmarty
thealmarty / PatternMatchingCompilerAlgorithm.md
Last active Sep 22, 2020
Efficient compilation of function definitions with pattern-matching using case-expressions.
View PatternMatchingCompilerAlgorithm.md

Efficient compilation of function definitions with pattern-matching

Function definitions with pattern-matching can be compiled into case-expressions for more efficient evaluation using the pattern matching compiler algorithm. The algorithm translates function definitions into case-expressions and avoids repeated examination of patterns.

I summarize the pattern matching compiler algorithm here as in chapter 5 of The implementation of functional programming languages.

The algorithm

A function definition of the form

@thealmarty
thealmarty / idris2unification.md
Last active Sep 14, 2020
Unification in Idris 2
View idris2unification.md

Unification in Idris 2

Unification concerns type/conversion checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicits (and implicit arguments) are inferred by unification.

Conversion checking (of terms and closures) determines whether the two inputs are equivalent. Similarly, unification determines whether the two inputs are equivalent with the presence of meta-variables. Naturally, unification is implemented as an extension to conversion checking.

@thealmarty
thealmarty / idris2notes.md
Last active Aug 4, 2021
Lessons from Idris 2
View idris2notes.md
View PLDI2020report.md

Potential Juvix features enabled by graph neural networks and machine learning

The rapid development of machine learning (ML) enables practical applications including in smart contract development. As a superior smart contract language, Juvix can provide extra support using ML in the following fronts:

  1. Generate correctness proofs

See this paper. When combining the mechanics of Proverbot9001, CoqHammer and CoqGym, a meaningful portion (28%) of the correctness proofs of CompCert (written in Coq) was generated. Note that the difficulties of the generated proofs are evenly distributed - i.e., it is not only generating proofs that are trivial for users to write.

Juvix is built with the intent that smart contracts written in it are more secure because users can write proofs to prove important properties of a contract. However, writing proofs is a tedious and costly task. Juvix would be much more attractive if it can write a significant portion of the proof

@thealmarty
thealmarty / token.liq
Last active Sep 17, 2019
A simplified token contract written in Liquidity, for deployment in the Tezos ledger.
View token.liq
type account = {
balance : nat;
allowances : (address, nat) map;
}
type storage = {
accounts : (address, account) big_map;
version : nat;
totalSupply : nat;
name : string;
@thealmarty
thealmarty / fact_s.hs
Last active Jan 28, 2019
Factorial function in Haskell.
View fact_s.hs
--Factorial function, short/standard version.
fact 0 = 1
fact n = n * fact (n - 1)
main = do
print (fact 5)