Skip to main content

Coronavirus (COVID-19) Updates | More Information

  • Library
  • Giving
  • Directories
  • Events
  • Directions
  • information for...
    • Current Students
    • Faculty and Staff
    • Parents and Families
    • Undergraduate Admissions
    • Graduate Admissions
Home
  • About
  • Academics
  • Admissions
  • Financial Aid
  • Student Life
  • Alumnae/i

You are here

  1. Home ›
  2. Bryn Mawr College News and Headlines ›
  3. Faculty Publication: Assistant Professor of Computer Science Richard A. Eisenberg

News

  • Bryn Mawr in the Media
  • Faculty Publications
  • Alumnae/i News
  • Athletics News
  • Mawrter Made Media
  • Events
  • Announcements
  • Class of 2020 Student Profiles

Faculty Publication: Assistant Professor of Computer Science Richard A. Eisenberg

Posted January 31st, 2019 at 3:29 pm

The Thoralf Plugin For Your Fancy Type Needs

Authors: Otwani, D; Eisenberg, RA

Source: ACM SIGPLAN NOTICES, 53 (7):106-118; 10.1145/3242744.3242754 JUL 2018

Publication Type: Article

Abstract: Many fancy types (e.g., generalized algebraic data types, type families) require a type checker plugin. These fancy types have a type index (e.g., type level natural numbers) with an equality relation that is difficult or impossible to represent using GHC's built-in type equality. The most practical way to represent these equality relations is through a plugin that asserts equality constraints. However, such plugins are difficult to write and reason about. In this paper, we (1) present a formal theory of reasoning about the correctness of type checker plugins for type indices, and, (2) apply this theory in creating Thoralf, a generic and extensible plugin for type indices that translates GHC constraint problems to queries to an external SMT solver. By "generic and extensible", we mean the restrictions on extending Thoralf are slight, and, if some type index could be encoded as an SMT sort, then a programmer could extend Thoralf by providing this encoding function.

Department of Computer Science

Related Stories

Faculty Publication: Assistant Professor of Psychology Heejung Park
Faculty Publication: Assistant Professor of Philosophy Thimo Heisenberg
Faculty Publication: Professor of Mathematics Paul Melvin
  • Twitter
  • LinkedIn
  • Facebook
  • Youtube
  • Instagram
  • About
  • Academics
  • Admissions
  • Financial Aid
  • Student Life
  • Alumnae/i
  • Library
  • Giving
  • Directories
  • Events
  • Directions
  • Jobs

Report a website issue

Web Accessibility Policy

Privacy Policy

Bryn Mawr College 101 North Merion Ave Bryn Mawr, PA 19010-2899
(610) 526-5000

Copyright © 2021

Give Now