BitC Documentation

The BitC Language and System

BitC (0.11 Transitional) Language Specification (Version 0.11+) [pdf]
Jonathan Shapiro, Ph.D., Swaroop Sridhar, Scott Doerrie

Provisional specification for the BitC programming language.

Version 0.11 is a transitional version that is working our the final surface syntax. This version of the language supports the old s-expression syntax and the new syntax simultaneously to ease transition.

BitC 0.10 Language Specification (Version 0.10+) [pdf]
Jonathan Shapiro, Ph.D., Swaroop Sridhar, Scott Doerrie

Specification for version 0.10 of the language. This is the last version that was s-expression based.

BitC Language Change History (Version 0.10) [pdf]
Jonathan Shapiro, Ph.D., Swaroop Sridhar, Scott Doerrie

History of changes to the BitC language design.

BitCC Release Notes (Version 0.9.1) [pdf]
Jonathan Shapiro, Ph.D., Swaroop Sridhar

Release notes for BitCC version 0.9.1.

The Origins of the BitC Programming Language (SRL Technical Report 2008-04)(Warning: Work in Progress) [pdf]
Jonathan Shapiro, Ph.D., Swaroop Sridhar, M. Scott Doerrie

Work in progress! Paper describing the purpose and key features of the BitC programming language.

Unicode Handling in BitC [pdf]
Jonathan Shapiro, Ph.D.

Describes how Unicode character handling works in BitC, and the assumptions behind our decisions.

Published Papers

Papers about Coyotos or BitC.

Programming Language Challenges in Systems Codes (Why Systems Programmers Still Use C, and What to Do About It) [pdf]
Jonathan Shapiro, Ph.D.

Dr. Shapiro's invited talk in PLOS 2006 workshop.

Sound and Complete Type Inference for a Systems Programming Language [pdf]
Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

APLAS 2008 paper describing the theory of BitC mutability model and type inference.

The HTML version of this paper is not able to represent all of the mathematical notation correctly.

Towards a Verified, General-Purpose Operating System Kernel [pdf]
Jonathan Shapiro, Ph.D., Michael Scott Doerrie, Eric Northup, Swaroop Sridhar, Mark Miller

Paper for the 2004 NICTA Operating Systems Verification Workshop. Describes our approach to creating a fully verified capability-based kernel and system.

Type Inference for Unboxed Types and First Class Mutability [pdf]
Swaroop Sridhar, Jonathan Shapiro, Ph.D.

PLOS 2006 workshop paper informally describing a heuristic approach to polymorphic type inference in the presence of unboxed mutability.

Technical Reports

Design of Type and Mutability Inference in BitC (SRL Technical Report SRL2006-01) [pdf]
Swaroop Sridhar, Jonathan Shapiro, Ph.D.

Discussion about the issues with type inference in the presence of unboxed mutability.

Formalization of the BitC Type System (SRL Technical Report SRL2007-01) [pdf]
Swaroop Sridhar, Jonathan S. Shapiro, Ph.D., Scott F. Smith, Ph.D.

Heuristic Type Inference in BitC (SRL Technical Report SRL2008-01) [pdf]
Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

A Theory of BitC mutability model and heuristic type inference algorithm.

The HTML version of this paper is not able to represent all of the mathematical notation correctly.

Sound Mutable and Const Types (SRL Technical Report SRL2008-03) [pdf]
Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

BitC semantics enhanced with const and correct handling of mutability such that sound, in-place references within unboxed structures can be supported.

The HTML version of this paper is not able to represent all of the mathematical notation correctly.

Sound and Complete Type Inference in BitC (SRL Technical Report SRL2008-02) [pdf]
Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

A longer version of the APLAS 2008 paper (describing sound and complete type inference in BitC) along with detailed proofs.

The HTML version of this paper is not able to represent all of the mathematical notation correctly.

The Compiler Implementation

Closure Implementation in BitC (Preliminary Implementation Note) [pdf]
Jonathan Shapiro, Ph.D.

Notes on closure construction for BitC.

Layout Handling in BitC [pdf]
Jonathan Shapiro, Ph.D.

Describes how layout is actually implemented in the bring-up version of the BitC compiler.

Polymorphism by Polyinstantiation (Preliminary Implementation Note) [pdf]
Jonathan Shapiro, Ph.D.

Discussion about the implementation level details of polyinstantiation in BitC.

Prototype Compiler Internals (Preliminary Notes) [pdf]
Jonathan Shapiro, Ph.D.

Quick note on the compiler passes and what they do.