Search Results

Documents authored by Weirich, Stephanie

Document
DOI: 10.4230/LIPIcs.TYPES.2019.7
Eta-Equivalence in Core Dependent Haskell

Authors: Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
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.
Cite as

Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kravchukkirilyuk_et_al:LIPIcs.TYPES.2019.7,
  author =	{Kravchuk-Kirilyuk, Anastasiya and Voizard, Antoine and Weirich, Stephanie},
  title =	{{Eta-Equivalence in Core Dependent Haskell}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{7:1--7:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7},
  URN =		{urn:nbn:de:0030-drops-130716},
  doi =		{10.4230/LIPIcs.TYPES.2019.7},
  annote =	{Keywords: Dependent types, Haskell, Irrelevance, Eta-equivalence}
}
Document
DOI: 10.4230/DagRep.6.3.59
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)

Authors: Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich

Published in: Dagstuhl Reports, Volume 6, Issue 3 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16131 "Language Based Verification Tools for Functional Programs". This seminar is motivated by two converging trends in computing -- the increasing reliance on software has led to an increased interest in seeking formal, reliable means of ensuring that programs possess crucial correctness properties, and the dramatic increase in adoption of higher-order functional languages due to the web, multicore and "big data" revolutions. While the research community has studied the problem of language based verification for imperative and first-order programs for decades – yielding important ideas like Floyd-Hoare Logics, Abstract Interpretation, Model Checking, and Separation Logic and so on – it is only relatively recently, that proposals have emerged for language baseverification tools for functional and higher-order programs. These techniques include advanced type systems, contract systems, model checking and program analyses specially tailored to exploit the structure of functional languages. These proposals are from groups based in diverse research communities, attacking the problem from different angles, yielding techniques with complementary strengths. This seminar brought diverse set of researchers together so that we could: compare the strengths and limitations of different approaches, discuss ways to unify the complementary advantages of different techniques, both conceptually and in tools, share challenging open problems and application areas where verification may be most effective, identify novel ways of using verification techniques for other software engineering tasks such as code search or synthesis, and improve the pedagogy and hence adoption of such techniques.
Cite as

Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, and Stephanie Weirich. Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). In Dagstuhl Reports, Volume 6, Issue 3, pp. 59-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{gaboardi_et_al:DagRep.6.3.59,
  author =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  title =	{{Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131)}},
  pages =	{59--77},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{6},
  number =	{3},
  editor =	{Gaboardi, Marco and Jagannathan, Suresh and Jhala, Ranjit and Weirich, Stephanie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.3.59},
  URN =		{urn:nbn:de:0030-drops-61494},
  doi =		{10.4230/DagRep.6.3.59},
  annote =	{Keywords: Functional Programming, Type Systems, Contracts, Dependent Types, Model Checking, Program Analysis}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.9
Combining Proofs and Programs

Authors: Stephanie Weirich

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Programming languages based on dependent type theory promise two great advances: flexibility and security. With the type-level computation afforded by dependent types, algorithms can be more generic, as the type system can express flexible interfaces via programming. Likewise, type-level computation can also express data structure invariants, so that programs can be proved correct through type checking. Furthermore, despite these extensions, programmers already know everything. Via the Curry-Howard isomorphism, the language of type-level computation and the verification logic is the programming language itself. There are two current approaches to the design of dependently-typed languages: Coq, Epigram, Agda, which grew out of the logics of proof assistants, require that all expressions terminate. These languages provide decidable type checking and strong correctness guarantees. In contrast, functional programming languages, like Haskell and Omega, have adapted the features dependent type theories, but retain a strict division between types and programs. These languages trade termination obligations for more limited correctness assurances. In this talk, I present a work-in-progress overview of the Trellys project. Trellys is new core language, designed to provide a smooth path from functional programming to dependently-typed programming. Unlike traditional dependent type theories and functional languages, Trellys allows programmers to work with total and partial functions uniformly. The language itself is composed of two fragments that share a common syntax and overlapping semantics: a simple logical language that guarantees total correctness and an expressive call-by-value programming language that guarantees types safety but not termination. Importantly, these two fragments interact. The logical fragment may soundly reason about effectful, partial functions. Program values may be used as evidence by the logic. We call this principle freedom of speech: whereas proofs themselves must terminate, they must be allowed to reason about any function a programmer might write. To retain consistency, the Trellys type system keeps track of where potentially non-terminating computations may appear, so that it can prevent them from being used as proofs.
Cite as

Stephanie Weirich. Combining Proofs and Programs. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, p. 9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{weirich:LIPIcs.RTA.2011.9,
  author =	{Weirich, Stephanie},
  title =	{{Combining Proofs and Programs}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{9--9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.9},
  URN =		{urn:nbn:de:0030-drops-31398},
  doi =		{10.4230/LIPIcs.RTA.2011.9},
  annote =	{Keywords: Dependent types, functional programming}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact