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 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 Eisenberg

Posted October 23rd, 2017 at 4:30 pm

A Specification for Dependent Types in Haskell

Authors: Weirich, Stephanie, Voizard, Antoine, Azevedo de Amorim, Pedro Henrique, and Eisenberg, Richard

Publication Type: Journal Article

Source: Proc. ACM Program. Lang. 1, 1, Article 31 (September 2017),https://doi.org/10.1145/3110275

Abstract: We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results -- chiefly, type safety, along with theorems that relate these two languages -- have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell’s term language does not correspond to a consistent logic.

Department of Computer Science

Related Stories

New Faculty: Christian Murphy, Senior Lecturer and Program Coordinator, Department of Computer Science
New Faculty: Assistant Professor of Computer Science Aline Normoyle
Summer Internship: Millicent Auma '21, Morgan Stanley
  • 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