2019/11/10 by Aditya Srinivasan, Srinivasan, Aditya, Andrew D. Hilton +1
Computer Science · Engineering · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Programming Languages (cs.PL) #VLSI and Analog Circuit Testing #VLSI and FPGA Design Techniques
paper · pdf · doi:10.48550/arxiv.1911.03926
openalex publication_date 2019/11/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.