Gemini: A Functional Programming Language for Hardware Description

TL;DR

Gemini is a novel functional programming language designed for hardware description, featuring advanced type systems and type inference to enhance expressivity and safety in modeling hardware and software constructs.

Contribution

It introduces a new type system with multiple atomic kinds and dependent types, along with formalizations and a prototype implementation for hardware description.

Findings

Formal grammar, typing, and evaluation rules established

Proof of safety for Gemini's type system

Prototype compiler implementation demonstrated

Abstract

This paper presents Gemini, a functional programming language for hardware description that provides features such as parametric polymorphism, recursive datatypes, higher-order functions, and type inference for higher expressivity compared to modern hardware description languages. Gemini demonstrates the theory and implementation of novel type-theoretical concepts through its unique type system consisting of multiple atomic kinds and dependent types, which allows the language to model both software and hardware constructs safely and perform type inference through multi-staged compilation. The primary technical results of this paper include formalizations of the Gemini grammar, typing rules, and evaluation rules, a proof of safety of Gemini's type system, and a prototype implementation of the compiler's semantic analysis phase.