ARTs (21)

Check out the Zenodo ART Collection for the latest published ARTs. Below, we provide a concise list of papers published in the ART repository.

Updated: 2024-12-30 02:28:10

Nock for Functional Programmers
Latest update: December 18, 2024
Nock, combinators, big-step operational semantics

Nock for Functional Programmers

Czajka, Lukasz

https://art.anoma.net/list#paper-14511714

10.5281/zenodo.14511714 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.14511713 )

Abstract: We present Nock using mainstream programming language theory notations and terminology. The intention is to make Nock more accessible and to outline its use as a compilation target for a high-level functional language....

Keywords: Nock, combinators, big-step operational semantics

Download sources: record/14511714/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-nock-functional-programmers,
    author    = { Czajka, Lukasz },
    title     = { {Nock for Functional Programmers} },
    journal   = { Anoma Research Topics },
    month     = { Dec },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { December 18, 2024 },
    doi       = { 10.5281/zenodo.14511714 },
    url       = { https://doi.org/10.5281/zenodo.14511713 }
}

Heterogeneous Paxos 2.0: the Specs
Latest update: December 04, 2024
Heterogeneous Paxos, distributed algorithm, consensus, Learner Graph

Heterogeneous Paxos 2.0: the Specs

Karbyshev, Aleksandr and Sheff, Isaac

https://art.anoma.net/list#paper-14276903

10.5281/zenodo.14276903 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.12572557 )

Abstract: We present Heterogeneous Paxos 2.0 (HP2.0), an improved version of Heterogeneous Paxos consensus algorithm (HP). In a nutshell, HP2.0 simplifies the algorithm logic, reduces bandwidth usage, and enables a more efficient implementation. HP2.0 is compatible with HP's requirements and has the same correctness properties. A formal specification of HP2.0 in TLA+ is available as a separate software artefact, with a formal proof of the key safety property of Agreement in TLAPS. This report provides an accessible account of HP2.0, of the design space in which it exists, and of the design choices that led us to our current system....

Keywords: Heterogeneous Paxos, distributed algorithm, consensus, Learner Graph

Download sources: record/14276903/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-heterogeneous-paxos-20-specs,
    author    = { Karbyshev, Aleksandr and Sheff, Isaac },
    title     = { {Heterogeneous Paxos 2.0: the Specs} },
    journal   = { Anoma Research Topics },
    month     = { Dec },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { December 04, 2024 },
    doi       = { 10.5281/zenodo.14276903 },
    url       = { https://doi.org/10.5281/zenodo.12572557 }
}

Other versions:

Message Logic
Latest update: December 04, 2024
Distributed Systems, Dynamic Modal Logic, Service Commitments

Message Logic

Gabbay, Murdoch J. and Zarin, Naqib

https://art.anoma.net/list#paper-14251398

10.5281/zenodo.14251398 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.14251397 )

Abstract: We introduce Message Logic, a dynamic modal logic for specifying and reasoning about message- passing in distributed systems. We study in particular how to express that participants make commitments to each other about their future behaviour. This leads us to develop a kind of ‘partial implication’ which we call pragmatic implication, and to an axiomatisation of the action of offering a commitment. We then discuss how this logic can be understood in the context of industrial practice....

Keywords: Distributed Systems, Dynamic Modal Logic, Service Commitments

Download sources: record/14251398/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-message-logic,
    author    = { Gabbay, Murdoch J. and Zarin, Naqib },
    title     = { {Message Logic} },
    journal   = { Anoma Research Topics },
    month     = { Dec },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { December 04, 2024 },
    doi       = { 10.5281/zenodo.14251398 },
    url       = { https://doi.org/10.5281/zenodo.14251397 }
}

Anoma State Architecture
Latest update: December 04, 2024
State Machine, Storage, Execution, Resource Machine

Anoma State Architecture

Sheff, Isaac

https://art.anoma.net/list#paper-14265827

10.5281/zenodo.14265827 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.14265826 )

Abstract: Each anoma instance maintains a state machine, which ultimately implements the Resource Machine. This is the state of that state machine. This state limits what can be done in post-ordering execution....

Keywords: State Machine, Storage, Execution, Resource Machine

Download sources: record/14265827/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-anoma-state-architecture,
    author    = { Sheff, Isaac },
    title     = { {Anoma State Architecture} },
    journal   = { Anoma Research Topics },
    month     = { Dec },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { December 04, 2024 },
    doi       = { 10.5281/zenodo.14265827 },
    url       = { https://doi.org/10.5281/zenodo.14265826 }
}

Slow Games: Policy Enforcement under Uncertainty
Latest update: September 15, 2024
Mechanism Design, Distributed Systems, Coding Theory

Slow Games: Policy Enforcement under Uncertainty

Reusche, D and Goes, Christopher and Della Penna, Nicolas

https://art.anoma.net/list#paper-13765214

10.5281/zenodo.13765214 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.13765213 )

Abstract: Motivated by decentralized permissionless protocols that are ultimately backed by social consensus, which can only perceive and act much slower than the service provisioning, we study what we term a Slow Game; a type of principal-agent problem, in which the agent acts as operator of a service and the principal as a regulator, which sets and attempts to enforce policies on the service being provided. The regulator is slower acting and measuring than the operator, which introduces uncertainty depending on the difference in speed. In this publication we introduce a framework inspired by lossy compression problems to model this type of game, as well as present results from simulations of a minimal example....

Keywords: Mechanism Design, Distributed Systems, Coding Theory

Download sources: record/13765214/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-slow-games-policy-enforcement-under,
    author    = { Reusche, D and Goes, Christopher and Della Penna, Nicolas },
    title     = { {Slow Games: Policy Enforcement under Uncertainty} },
    journal   = { Anoma Research Topics },
    month     = { Sep },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { September 15, 2024 },
    doi       = { 10.5281/zenodo.13765214 },
    url       = { https://doi.org/10.5281/zenodo.13765213 }
}

Comparing Two Hash Functions for Multi-Party Computation and Zero-Knowledge
Latest update: September 10, 2024
Hydra, Poseidon, MPC, ZKP

Comparing Two Hash Functions for Multi-Party Computation and Zero-Knowledge

Yıldız, Burcu and Maller, Mary

https://art.anoma.net/list#paper-13739511

10.5281/zenodo.13739511 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.13739510 )

Abstract: Cryptographic hash functions are a paramount building block in cryptography and are used for numerous applications. The hash function Poseidon is widely favored for zero-knowledge applications (e.g. FileCoin, Dusk Network, LoopRing), and has been tailor designed for this purpose. The hash function Hydra is optimized to be computed in MPC. Hydra was presented in Eurocrypt 2023 and has less total number of rounds and transmitted data than its competitors. Zero knowledge and MPC applications that prove or compute hash functions share many similarities in terms of the optimization criteria of the function. For applications that require both proving a hash function in zero-knowledge and computing a hash function in MPC we ask the natural question: How do the hash functions Poseidon and Hydra, which are optimized for zero-knowledge and MPC applications, respectively, perform for the other application? To answer this...

Keywords: Hydra, Poseidon, MPC, ZKP

Download sources: record/13739511/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-comparing-two-hash-functions,
    author    = { Yıldız, Burcu and Maller, Mary },
    title     = { {Comparing Two Hash Functions for Multi-Party Computation and Zero-Knowledge} },
    journal   = { Anoma Research Topics },
    month     = { Sep },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { September 10, 2024 },
    doi       = { 10.5281/zenodo.13739511 },
    url       = { https://doi.org/10.5281/zenodo.13739510 }
}

Compiling Juvix to Cairo Assembly
Latest update: September 10, 2024
Cairo, Starknet, Anoma, Juvix, Compilers, Zero-knowledge Proofs, Functional programming

Compiling Juvix to Cairo Assembly

Czajka, Łukasz

https://art.anoma.net/list#paper-13739344

10.5281/zenodo.13739344 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.13739343 )

Abstract: We describe a pipeline for compiling the functional programming language Juvix to the bytecode of the Cairo~VM, which enables zero-knowledge proofs of Juvix program execution. The read-only memory model of Cairo fits well with the purely functional nature of Juvix, but also presents some unique challenges....

Keywords: Cairo, Starknet, Anoma, Juvix, Compilers, Zero-knowledge Proofs, Functional programming

Download sources: record/13739344/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-compiling-juvix-cairo-assembly,
    author    = { Czajka, Łukasz },
    title     = { {Compiling Juvix to Cairo Assembly} },
    journal   = { Anoma Research Topics },
    month     = { Sep },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { September 10, 2024 },
    doi       = { 10.5281/zenodo.13739344 },
    url       = { https://doi.org/10.5281/zenodo.13739343 }
}

Intent-centric Applications for the Anoma Resource Machine
Latest update: August 26, 2024
Anoma Resource Machine, Resource Model, Anoma Applications

Intent-centric Applications for the Anoma Resource Machine

Heuer, Michael and Reusche, D

https://art.anoma.net/list#paper-13340448

10.5281/zenodo.13340448 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.13340447 )

Abstract: Anoma introduces a universal intent machine, allowing developers to write applications in terms of intents, which can be ordered, solved, and settled anywhere. This work illustrates how intent-centric applications can be built using the Juvix language in Anoma’s resource model and in compliance with the Anoma resource machine. First, we detail the general architecture of applications and their relation to and dependencies on other components of the Anoma protocol. Second, we describe recurring design patterns and primitives related to resource creation and initialization, authorization, ownership, intents, and tokens in a broader context. Last, and by employing these primitives, we present Kudos, an accounting primitive incorporating trust relationships between identities....

Keywords: Anoma Resource Machine, Resource Model, Anoma Applications

Download sources: record/13340448/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-intentcentric-applications-anoma,
    author    = { Heuer, Michael and Reusche, D },
    title     = { {Intent-centric Applications for the Anoma Resource Machine} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { August 26, 2024 },
    doi       = { 10.5281/zenodo.13340448 },
    url       = { https://doi.org/10.5281/zenodo.13340447 }
}

Heterogeneous Narwhal and Paxos
Latest update: June 27, 2024
heterogeneous protocols, typhon, interoperability, protocol integration, consensus, cross-chain, heterogeneous trust

Heterogeneous Narwhal and Paxos

Heindel, Tobias and Karbyshev, Aleksandr and Sheff, Isaac

https://art.anoma.net/list#paper-10498999

10.5281/zenodo.10498999 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10498998 )

Abstract: Blockchain interoperability often requires a mutually trusted layer (in the case of roll-ups or side-chains), or a third party (in the case of bridges). Heterogeneous Consensus protocols introduced the possibility for more direct, decentralized interoperability: chains can commit transactions together, given "enough" overlap in their trust assumptions. Like a bridge, such protocols ensure atomicity under specific trust conditions. Unlike a bridge, chains never relinquish control over the safety or liveness of their data. However, consensus is only part of the story: efficient mempool architectures like Narwhal can dramatically improve scalability and increase chain throughput. However, these mempools also rely on the chain's underlying trust assumptions. We generalize Narwhal for a Heterogeneous Trust model, and explain how to use it with Heterogeneous Paxos to commit cross-chain atomic transactions....

Keywords: heterogeneous protocols, typhon, interoperability, protocol integration, consensus, cross-chain, heterogeneous trust

Download sources: record/10498999/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-heterogeneous-narwhal-paxos,
    author    = { Heindel, Tobias and Karbyshev, Aleksandr and Sheff, Isaac },
    title     = { {Heterogeneous Narwhal and Paxos} },
    journal   = { Anoma Research Topics },
    month     = { Jun },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { June 27, 2024 },
    doi       = { 10.5281/zenodo.10498999 },
    url       = { https://doi.org/10.5281/zenodo.10498998 }
}

Cross-Chain Integrity with Controller Labels and Endorsement
Latest update: June 25, 2024
controllers, distributed systems, network management, system architecture

Cross-Chain Integrity with Controller Labels and Endorsement

Isaac, Sheff

https://art.anoma.net/list#paper-10498997

10.5281/zenodo.10498997 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10498996 )

Abstract: In distributed systems, mutable digital objects typically require some state machine to decide on their definitive current state. This state machine can be replicated to enhance availability and fault tolerance. We call the authoritative state machine of a digital object its controller. Typical examples of controllers defining objects include a database storing a record or a blockchain storing the current state of a smart contract. Without some kind of controller, different parties may have contradictory notions of what the state is and no way to reconcile them. In a distributed system, some controllers may be Byzantine, and make duplicitous or incoherent statements about the state. Here we design rules and procedures for a multi-state-machine ecosystem featuring digital objects or resources, with application-defined state-dependent rules for how they can be updated. Each controller can express an authoritative state, including authoritative resource...

Keywords: controllers, distributed systems, network management, system architecture

Download sources: record/10498997/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-crosschain-integrity-controller-labels,
    author    = { Isaac, Sheff },
    title     = { {Cross-Chain Integrity with Controller Labels and Endorsement} },
    journal   = { Anoma Research Topics },
    month     = { Jun },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { June 25, 2024 },
    doi       = { 10.5281/zenodo.10498997 },
    url       = { https://doi.org/10.5281/zenodo.10498996 }
}

Anoma Resource Machine Specification
Latest update: June 25, 2024
anoma, blockchain technology, protocol design, resource machine

Anoma Resource Machine Specification

Khalniyazova, Yulia and Goes, Christopher

https://art.anoma.net/list#paper-10689620

10.5281/zenodo.10689620 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10498990 )

Abstract: The article explores the Anoma Resource Machine (ARM) within the Anoma protocol, providing a comprehensive understanding of its role in facilitating state updates based on user preferences. Drawing parallels with the Ethereum Virtual Machine, the ARM introduces a flexible transaction model, diverging from traditional account and UTXO models. Key properties such as atomic state transitions, information flow control, account abstraction, and an intent-centric architecture contribute to the ARM's robustness and versatility. Inspired by the Zcash protocol, the ARM leverages commitment accumulators to ensure transaction privacy. The article outlines essential building blocks, computable components, and requirements for constructing the ARM, highlighting its unique approach to resource-based state management....

Keywords: anoma, blockchain technology, protocol design, resource machine

Download sources: record/10689620/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-anoma-resource-machine-specification,
    author    = { Khalniyazova, Yulia and Goes, Christopher },
    title     = { {Anoma Resource Machine Specification} },
    journal   = { Anoma Research Topics },
    month     = { Jun },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { June 25, 2024 },
    doi       = { 10.5281/zenodo.10689620 },
    url       = { https://doi.org/10.5281/zenodo.10498990 }
}

Other versions:

Compiling to ZKVMs
Latest update: April 19, 2024
zero-knowledge proofs, zkVM, virtual machines, privacy-preserving computation

Compiling to ZKVMs

Centelles, Alberto

https://art.anoma.net/list#paper-10998758

10.5281/zenodo.10998758 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10498994 )

Abstract: With the advent of non-uniform folding schemes, the lookup singularity, generalised arithmetisations such as CCS and the application of towers of binary fields to SNARKs, many of the existing assumptions on SNARKs have been put into question, and the design space of zkVMs has opened. Although zkVMs provide a friendly developer experience, their proving time is still significantly (around a million times) slower than direct compilation to circuits due to the overhead of their abstractions (stack, memory, execution unit, etc). One of the causes of their poor performance is that existing zkVMs are still program agnostic; their provers haven't leveraged the structure of a program. Compilers have a long history of optimising computations by identifying patterns in their structure. We take advantage of the fact that a program is generally executed before it is proven, so the prover of a...

Keywords: zero-knowledge proofs, zkVM, virtual machines, privacy-preserving computation

Download sources: record/10998758/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-compiling-zkvms,
    author    = { Centelles, Alberto },
    title     = { {Compiling to ZKVMs} },
    journal   = { Anoma Research Topics },
    month     = { Apr },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { April 19, 2024 },
    doi       = { 10.5281/zenodo.10998758 },
    url       = { https://doi.org/10.5281/zenodo.10498994 }
}

Other versions:

Intent Machines
Latest update: February 21, 2024
intent machine, user intentions, automation, machine learning

Intent Machines

Hart, Anthony and Reusche, D

https://art.anoma.net/list#paper-10654543

10.5281/zenodo.10654543 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10498992 )

Abstract: This paper serves as an overview of the abstract mathematical structures that may be used to formalize intents and the machines that process them. We will give a hierarchy of progressively more specific structures with the goal of capturing the concept of an abstract intent machine at different levels of abstraction, and use these insights to understand different methods for composing/combining/coordinating these machines....

Keywords: intent machine, user intentions, automation, machine learning

Download sources: record/10654543/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2024-intent-machines,
    author    = { Hart, Anthony and Reusche, D },
    title     = { {Intent Machines} },
    journal   = { Anoma Research Topics },
    month     = { Feb },
    year      = { 2024 },
    publisher = { Zenodo },
    version   = { February 21, 2024 },
    doi       = { 10.5281/zenodo.10654543 },
    url       = { https://doi.org/10.5281/zenodo.10498992 }
}

Other versions:

VampIR Bestiary
Latest update: November 13, 2023
VAMP-IR, Intermediate Representations, Three-address code (3AC), Rank-1 Constraint System (R1CS), AirScript

VampIR Bestiary

Fitzgerald, Joshua and Centelles, Alberto

https://art.anoma.net/list#paper-10118865

10.5281/zenodo.10118865 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10118864 )

Abstract: This report delves into the comprehensive study of VAMP-IR Modules, detailing their transformations and comparisons. It explores specific aspects such as definitions, expressions, constraints, auxiliary data, and related algorithms. A thorough examination of IRs and their roles in Vamp-IR is conducted, complete with trade-offs and discussions on IRs resembling a proof system. The document illustrates the relationship among the presented IRs through diagrams, alongside an ideal pipeline. Existing and potential Vamp-IRs like Initial IR, Three-address code (3AC), Evaluated, Eliminated, Partially Evaluated and Partially Flattened (PEPF), Plonkish, R1CS, and AirScript are also discussed....

Keywords: VAMP-IR, Intermediate Representations, Three-address code (3AC), Rank-1 Constraint System (R1CS), AirScript

Download sources: record/10118865/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-vampir-bestiary,
    author    = { Fitzgerald, Joshua and Centelles, Alberto },
    title     = { {VampIR Bestiary} },
    journal   = { Anoma Research Topics },
    month     = { Nov },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { November 13, 2023 },
    doi       = { 10.5281/zenodo.10118865 },
    url       = { https://doi.org/10.5281/zenodo.10118864 }
}

Constraint Satisfaction Problems: A Survey for Anoma
Latest update: October 18, 2023
Constraint Satisfaction, Intents, Formal Logic, Automated Reasoning, Surveys

Constraint Satisfaction Problems: A Survey for Anoma

Hart, Anthony

https://art.anoma.net/list#paper-10019113

10.5281/zenodo.10019113 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.10019112 )

Abstract: This paper serves as a broad introduction to Constraint Satisfaction Problems (CSPs) tailored for professionals working on Anoma, a decentralized financial framework. Our primary aim is to build a robust intuition for CSPs, preparing the Anoma community for its application in optimizing intents—defined as desires for future states of the financial system. We explore a wide array of CSP examples, including but not limited to Boolean Satisfiability and Integer Linear Programming, to equip readers with a general understanding of the field. We also include an overview of CSP tractability, aiming to give the reader an understanding of the limitations of solvability. A unique emphasis is placed on compositional methods, facilitating distributed problem-solving across multiple agents. Towards the end, we formalize the notion of 'intents' within the framework of Constraint Optimization....

Keywords: Constraint Satisfaction, Intents, Formal Logic, Automated Reasoning, Surveys

Download sources: record/10019113/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-constraint-satisfaction-problems-survey,
    author    = { Hart, Anthony },
    title     = { {Constraint Satisfaction Problems: A Survey for Anoma} },
    journal   = { Anoma Research Topics },
    month     = { Oct },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { October 18, 2023 },
    doi       = { 10.5281/zenodo.10019113 },
    url       = { https://doi.org/10.5281/zenodo.10019112 }
}

Exploring Cryptographic Approaches to Enhance Privacy in Intent Solving
Latest update: October 02, 2023
Collaborative SNARKs, Functional encryption, Homomorphic encryption, Intents, Multiparty computation, Searchable encryption, Private solving, Trusted execution environment, Witness encryption

Exploring Cryptographic Approaches to Enhance Privacy in Intent Solving

Khalniyazova, Yulia

https://art.anoma.net/list#paper-8321167

10.5281/zenodo.8321167 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8321166 )

Abstract: This report explores cryptographic strategies that could enhance privacy while solving intents in Anoma. We consider well-known solutions like trusted execution environment, multiparty computations and homomorphic encryption and more exotic primitives like functional encryption, witness encryption, searchable encryption and collaborative SNARKs. We identify the limiting factors for each primitive and provide a summary of the results....

Keywords: Collaborative SNARKs, Functional encryption, Homomorphic encryption, Intents, Multiparty computation, Searchable encryption, Private solving, Trusted execution environment, Witness encryption

Download sources: record/8321167/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-exploring-cryptographic-approaches-enhance,
    author    = { Khalniyazova, Yulia },
    title     = { {Exploring Cryptographic Approaches to Enhance Privacy in Intent Solving} },
    journal   = { Anoma Research Topics },
    month     = { Oct },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { October 02, 2023 },
    doi       = { 10.5281/zenodo.8321167 },
    url       = { https://doi.org/10.5281/zenodo.8321166 }
}

The Core language of Juvix
Latest update: August 29, 2023
Juvix, Functional programming, Compilers, Language specification, Lambda Calculus

The Core language of Juvix

Lukasz Czajka

https://art.anoma.net/list#paper-8268850

10.5281/zenodo.8268850 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8268849 )

Abstract: We describe JuvixCore -- a minimalistic intermediate functional language to which Juvix desugars. We specify precisely and abstractly JuvixCore syntax, evaluation semantics, and the current optional type system. We comment on the relationship between this specification and the actual implementation. We also explain the role JuvixCore plays in the Juvix compilation pipeline. Finally, we compare the language features available in JuvixCore with those in Juvix and other popular functional languages....

Keywords: Juvix, Functional programming, Compilers, Language specification, Lambda Calculus

Download sources: record/8268850/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-core-language-juvix,
    author    = { Lukasz Czajka },
    title     = { {The Core language of Juvix} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { August 29, 2023 },
    doi       = { 10.5281/zenodo.8268850 },
    url       = { https://doi.org/10.5281/zenodo.8268849 }
}

Other versions:

Rethinking VampIR
Latest update: August 29, 2023
VampIR, Arithmetic Circuits, Compilers, Proposals

Rethinking VampIR

Anthony Hart

https://art.anoma.net/list#paper-8262815

10.5281/zenodo.8262815 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8262814 )

Abstract: This paper provides an overview of VampIR v0.1.3 and outlines potential modifications for future versions. Specifically, it contains proposals for streamlined versions of the fresh function and constraint generation, a proposal for removing the type system, and a short proposal for dealing with imports. It ends with an overview of implementation improvements made in light of the Haskell port....

Keywords: VampIR, Arithmetic Circuits, Compilers, Proposals

Download sources: record/8262815/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-rethinking-vampir,
    author    = { Anthony Hart },
    title     = { {Rethinking VampIR} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { August 29, 2023 },
    doi       = { 10.5281/zenodo.8262815 },
    url       = { https://doi.org/10.5281/zenodo.8262814 }
}

Anoma: a unified architecture for full-stack decentralised applications
Latest update: August 24, 2023
Anoma, Intent-Centricity and Homogeneous Architecture, Full-Stack Decentralised Applications, Counterparty Discovery, Programmable Settlement Architectures

Anoma: a unified architecture for full-stack decentralised applications

Christopher Goes and Awa Sun Yin and Adrian Brink

https://art.anoma.net/list#paper-8279842

10.5281/zenodo.8279842 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8279841 )

Abstract: Programmable settlement architectures do not enable counterparty discovery and solving, both of which are necessary to build the majority of interactive multi-party applications. The architectural constraints of programmable settlement result in contemporary application protocols that have at least one Web2 component, which becomes the centralisation point. We present Anoma, a unified architecture for full-stack decentralised applications. Anoma is designed following the principles of intent-centricity and homogeneous architecture / heterogeneous security, together constituting a declarative paradigm for building decentralised applications. In this paper, we first outline the Anoma architecture, provide an intuition for the design rationale, and describe how Anoma disentangles the choices of protocol and security. We then define the Anoma application programming model and enumerate several existing and novel decentralised applications that can be built using the novel primitives. Finally, we outline the current components used to instantiate Anoma...

Keywords: Anoma, Intent-Centricity and Homogeneous Architecture, Full-Stack Decentralised Applications, Counterparty Discovery, Programmable Settlement Architectures

Download sources: record/8279842/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-anoma-unified-architecture,
    author    = { Christopher Goes and Awa Sun Yin and Adrian Brink },
    title     = { {Anoma: a unified architecture for full-stack decentralised applications} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { August 24, 2023 },
    doi       = { 10.5281/zenodo.8279842 },
    url       = { https://doi.org/10.5281/zenodo.8279841 }
}

Geb Pipeline
Latest update: August 21, 2023
Geb, Juvix, VampIR, compilers, category theory, semantics of PL, Lambda calculus, Arithmetic circuits

Geb Pipeline

Artem Gureev and Jonathan Prieto-Cubides

https://art.anoma.net/list#paper-8262747

10.5281/zenodo.8262747 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8262746 )

Abstract: At Heliax, we are developing a compiler stack to facilitate the creation of decentralized applications using high-level functional programming languages. This stack comprises a series of compilers that begin with Juvix and culminate in arithmetic circuits, represented via VampIR, an intermediate language for such circuits. This report highlights the Geb project, a component of this pipeline, and details the process of compiling JuvixCore into VampIR through the Geb compiler. To aid its adoption and implementation, we provide a categorical overview of the mathematical foundations of the Geb project and insights into its current Lisp-based implementation. The objective of this report is to guide future implementations and improvements of the Geb project....

Keywords: Geb, Juvix, VampIR, compilers, category theory, semantics of PL, Lambda calculus, Arithmetic circuits

Download sources: record/8262747/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-geb-pipeline,
    author    = { Artem Gureev and Jonathan Prieto-Cubides },
    title     = { {Geb Pipeline} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { August 21, 2023 },
    doi       = { 10.5281/zenodo.8262747 },
    url       = { https://doi.org/10.5281/zenodo.8262746 }
}

Juvix to VampIR Pipeline
Latest update: August 14, 2023
juvix, vamp-ir, geb, compilation, normalisation

Juvix to VampIR Pipeline

Lukasz Czajka

https://art.anoma.net/list#paper-8246536

10.5281/zenodo.8246536 (use this DOI to cite this version) (for all versions: 10.5281/zenodo.8246535 )

Abstract: This report explores two alternatives to Geb for Juvix-to-VampIR compilation. The first alternative is a straightforward approach based on full normalisation, which may be implemented relatively quickly and used as a comparison baseline for all other approaches. The second alternative is based on a pipeline of several compiler transformations that together convert Juvix programs into a form that can be directly translated to VampIR input....

Keywords: juvix, vamp-ir, geb, compilation, normalisation

Download sources: record/8246536/files-archive.zip

Share: LinkedIn | By email

BiBTeX:

@article{ art-2023-juvix-vampir-pipeline,
    author    = { Lukasz Czajka },
    title     = { {Juvix to VampIR Pipeline} },
    journal   = { Anoma Research Topics },
    month     = { Aug },
    year      = { 2023 },
    publisher = { Zenodo },
    version   = { August 14, 2023 },
    doi       = { 10.5281/zenodo.8246536 },
    url       = { https://doi.org/10.5281/zenodo.8246535 }
}

Other versions: