2026-07-23T08:31:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13071 2024-03-06T10:51:13Z ddc:004 open_access

Eta-Equivalence in Core Dependent Haskell Kravchuk-Kirilyuk, Anastasiya Voizard, Antoine Weirich, Stephanie Dependent types Haskell Irrelevance Eta-equivalence We extend the core semantics for Dependent Haskell with rules for η-equivalence. This semantics is defined by two related calculi, Systems D and DC. 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 the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anastasiya Kravchuk-Kirilyuk and Antoine Voizard and Stephanie Weirich 2020 Is Part Of LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2019.7 urn:nbn:de:0030-drops-130716 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7 eng https://creativecommons.org/licenses/by/3.0/legalcode