More Web Proxy on the site http://driver.im/

research-article

Guilt free ivory

Authors:

Trevor Elliott,

John LaunchburyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 12

Pages 189 - 200

https://doi.org/10.1145/2887747.2804318

Published: 30 August 2015 Publication History

Abstract

Ivory is a language that enforces memory safety and avoids most undefined behaviors while providing low-level control of memory- manipulation. Ivory is embedded in a modern variant of Haskell, as implemented by the GHC compiler. The main contributions of the paper are two-fold. First, we demonstrate how to embed the type-system of a safe-C language into the type extensions of GHC. Second, Ivory is of interest in its own right, as a powerful language for writing high-assurance embedded programs. Beyond invariants enforced by its type-system, Ivory has direct support for model-checking, theorem-proving, and property-based testing. Ivory’s semantics have been formalized and proved to guarantee memory safety.

References

[1]

ad. Website http://hackage.haskell.org/package/ad. Retrieved Feb. 2015.

[2]

estimator. Website http://hackage.haskell.org/ package/estimator. Retrieved Feb. 2015.

[3]

ghc-srcspan-plugin. Website http://hackage.haskell.org/ package/ghc-srcspan-plugin. Retrieved Feb. 2015.

[4]

linear. Website http://hackage.haskell.org/package/ linear. Retrieved Feb. 2015.

[5]

Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.

Digital Library

[6]

Heartbleed. http://heartbleed.com/, February 2015.

[7]

E. Axelsson, K. Claessen, M. Sheeran, J. Svenningsson, D. Engdal, and A. Persson. The design and implementation of Feldspar - an embedded language for digital signal processing. In Implementation and Application of Functional Languages, volume 6647 of LNCS, pages 121–136. Springer, 2011.

Digital Library

[8]

J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, 2003.

Digital Library

[9]

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification, pages 171–177, 2011.

Digital Library

[10]

S. Checkoway, D. McCoy, B. Kantor, D. Anderson, H. Shacham, S. Savage, K. Koscher, A. Czeskis, F. Roesner, and T. Kohno. Comprehensive experimental analyses of automotive attack surfaces. In USENIX Security, 2011.

Digital Library

[11]

K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In ACM SIGPLAN Notices, pages 268–279. ACM, 2000.

Digital Library

[12]

I. S. Diatchki and M. P. Jones. Strongly typed memory areas programming systems-level data structures in a functional language. In Proceedings of the ACM SIGPLAN Workshop on Haskell, pages 72–83. ACM, 2006.

Digital Library

[13]

I. S. Diatchki, M. P. Jones, and R. Leslie. High-level views on lowlevel representations. In Intl. Conference on Functional Programming, pages 168–179. ACM, 2005.

Digital Library

[14]

G. Eakman, H. Reubenstein, T. Hawkins, M. Jain, and P. Manolios. Practical formal verification of domain-specific language applications. In NASA Formal Methods Symposium. Springer, 2015.

[15]

L. Erkok. SBV: SMT based verification in Haskell. Website, 2014. http://leventerkok.github.io/sbv/.

[16]

S. Frazzetta and M. Pacino. A STANAG 4586 oriented approach to UAS navigation - the case of Italian Sky-Y flight trials. Journal of Intelligent and Robotic Systems, 69:21–31, 2013.

Digital Library

[17]

T. Hawkins. Controlling hybrid vehicles with Haskell. Presentation. Commercial Users of Functional Programming (CUFP), 2008. Available at http://cufp.galois.com/2008/schedule.html.

[18]

P. C. Hickey, L. Pike, T. Elliott, J. Bielman, and J. Launchbury. Building embedded systems with embedded DSLs (experience report). In Intl. Conference on Functional Programming (ICFP). ACM, 2014.

Digital Library

[19]

T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In USENIX Conference, Berkeley, CA, USA, 2002. USENIX.

Digital Library

[20]

JPL. JPL institutional coding standard for the C programming language. Technical Report JPL DOCID D-60411, Jet Propulsion Laboratory, 2009. Available at http://lars-lab.jpl.nasa.gov/ JPL_Coding_Standard_C.pdf.

[21]

M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. Kluwer, 2000.

Digital Library

[22]

O. Kiselyov and C.-c. Shan. Lightweight monadic regions. In Proceedings of the First ACM SIGPLAN Symposium on Haskell, Haskell ’08, pages 1–12, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-064-7. URL http://doi.acm.org/10.1145/ 1411286.1411288.

Digital Library

[23]

O. Kiselyov, A. Sabry, and C. Swords. Extensible effects: An alternative to monad transformers. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Haskell ’13, pages 59–70. ACM, 2013.

Digital Library

[24]

J. Launchbury and S. L. Peyton Jones. Lazy functional state threads. pages 24–35, June 1994.

Digital Library

[25]

J. R. Lewis, J. Launchbury, E. Meijer, and M. B. Shields. Implicit parameters: Dynamic scoping with static types. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 108–118. ACM, 2000.

Digital Library

[26]

S. Lindley and C. McBride. Hasochism: The pleasure and pain of dependently typed haskell programming. In Symposium on Haskell, pages 81–92. ACM, 2013.

Digital Library

[27]

J. P. Magalh˜aes. The right kind of generic programming. In Proceedings of the 8th ACM SIGPLAN Workshop on Generic Programming, WGP ’12, pages 13–24, New York, NY, USA, 2012. ACM. ISBN 978-1-4503-1576-0.

Digital Library

[28]

G. Mainland. Why it’s nice to be quoted: Quasiquoting for Haskell. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop, pages 73–82. ACM, 2007.

Digital Library

[29]

N. D. Matsakis and F. S. Klock, II. The Rust language. Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology, 34(3):103–104, Oct. 2014.

Digital Library

[30]

T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. ISBN 3-540-43376-7.

[31]

L. Pike, A. Goodloe, R. Morisset, and S. Niller. Copilot: A hard realtime runtime monitor. In Runtime Verification (RV), volume 6418, pages 345–359. Springer, 2010.

Digital Library

[32]

T. Schrijvers, S. Peyton Jones, M. Chakravarty, and M. Sulzmann. Type checking with open type functions. Intl. Conference on Functional Programming, pages 51–62, Sept. 2008. ISSN 0362-1340.

Digital Library

[33]

S. Sridhar. BitC: A Safe Systems Programming Language. PhD thesis, 2009.

Digital Library

[34]

B. A. Yorgey, S. Weirich, J. Cretin, S. Peyton Jones, D. Vytiniotis, and J. P. Magalh˜aes. Giving Haskell a promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI ’12, pages 53–66. ACM, 2012.

Digital Library

Cited By

Young DGrebe MGill A(2021)On Adding Pattern Matching to Haskell-Based Deeply Embedded Domain Specific LanguagesPractical Aspects of Declarative Languages10.1007/978-3-030-67438-0_2(20-36)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-67438-0_2
Ceresa MGorostiaga FSánchez C(2020)Declarative Stream Runtime Verification (hLola)Programming Languages and Systems10.1007/978-3-030-64437-6_2(25-43)Online publication date: 30-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64437-6_2
Mista ARusso A(2020)BinderAnn: Automated Reification of Source Annotations for Monadic EDSLsTrends in Functional Programming10.1007/978-3-030-57761-2_2(25-46)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_2
Show More Cited By

Index Terms

Guilt free ivory
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types

Recommendations

Building embedded systems with embedded DSLs
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

We report on our experiences in synthesizing a fully-featured autopilot from embedded domain-specific languages (EDSLs) hosted in Haskell. The autopilot is approximately 50k lines of C code generated from 10k lines of EDSL code and includes control laws,...
Guilt free ivory
Haskell '15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell

Ivory is a language that enforces memory safety and avoids most undefined behaviors while providing low-level control of memory- manipulation. Ivory is embedded in a modern variant of Haskell, as implemented by the GHC compiler. The main contributions ...
LibDSL: a library for developing embedded domain specific languages in d via template metaprogramming
GPCE '14

This paper presents a library called LibDSL that helps the implementer of an embedded domain specific language (EDSL) effectively develop it in D language. The LibDSL library accepts as input some kinds of ``specifications'' of the EDSL that the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 12

Haskell '15

December 2015

212 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2887747

Editor:
Matthew Fluet
Rochester Institute of Technology

Issue’s Table of Contents

Haskell '15: Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell
August 2015
212 pages
ISBN:9781450338080
DOI:10.1145/2804302
Program Chair:
Ben Lippmeier

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 August 2015

Published in SIGPLAN Volume 50, Issue 12

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

DARPA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
288
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)3

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Young DGrebe MGill A(2021)On Adding Pattern Matching to Haskell-Based Deeply Embedded Domain Specific LanguagesPractical Aspects of Declarative Languages10.1007/978-3-030-67438-0_2(20-36)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-67438-0_2
Ceresa MGorostiaga FSánchez C(2020)Declarative Stream Runtime Verification (hLola)Programming Languages and Systems10.1007/978-3-030-64437-6_2(25-43)Online publication date: 30-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64437-6_2
Mista ARusso A(2020)BinderAnn: Automated Reification of Source Annotations for Monadic EDSLsTrends in Functional Programming10.1007/978-3-030-57761-2_2(25-46)Online publication date: 18-Aug-2020
https://doi.org/10.1007/978-3-030-57761-2_2
Lubbers MKoopman PPlasmeijer R(2019)Multitasking on Microcontrollers using Task Oriented Programming2019 42nd International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO)10.23919/MIPRO.2019.8756711(1587-1592)Online publication date: May-2019
https://doi.org/10.23919/MIPRO.2019.8756711
Grebe MGill A(2019)Threading the Arduino with HaskellMicrobial Metabolic Engineering10.1007/978-3-030-14805-8_8(135-154)Online publication date: 21-Feb-2019
https://doi.org/10.1007/978-3-030-14805-8_8
Koopman PLubbers MPlasmeijer R(2018)A Task-Based DSL for MicrocomputersProceedings of the Real World Domain Specific Languages Workshop 201810.1145/3183895.3183902(1-11)Online publication date: 24-Feb-2018
https://dl.acm.org/doi/10.1145/3183895.3183902
Grebe MGill A(2016)Haskino: A Remote Monad for Programming the ArduinoPractical Aspects of Declarative Languages10.1007/978-3-319-28228-2_10(153-168)Online publication date: 9-Jan-2016
https://doi.org/10.1007/978-3-319-28228-2_10
Li STrinder PDe Troyer CLubbers MRamsingh AFernandez-Reyes KVoinea A(2024)The Benefits of Tierless Elixir/Potato for Engineering IoT SystemsProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678197(84-95)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678197
Lubbers MKoopman PRamsingh ASinger JTrinder P(2023)Could Tierless Languages Reduce IoT Development Grief?ACM Transactions on Internet of Things10.1145/35729014:1(1-35)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3572901
Valliappan NKrook RRusso AClaessen KSchrijvers T(2020)Towards secure IoT programming in HaskellProceedings of the 13th ACM SIGPLAN International Symposium on Haskell10.1145/3406088.3409027(136-150)Online publication date: 27-Aug-2020
https://dl.acm.org/doi/10.1145/3406088.3409027
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents