- Haskell-Cafe - Haskell.org

FMBC 2021 - 2nd Call for Papers
by Bruno Bernardo 10 Apr '21

10 Apr '21

[ Please distribute, apologies for multiple postings. ] ======================================================================== 3rd International Workshop on Formal Methods for Blockchains (FMBC) - Second Call https://fmbc.gitlab.io/2021 July 18 or 19 (TBA), 2021 Co-located with the 33nd International Conference on Computer-Aided Verification (CAV 2021) http://i-cav.org/2021/ ------------------------------------------------------------- IMPORTANT DATES -------------------------------- Abstract submission: April 22, 2021 Full paper submission: April 29, 2021 Notification: June 10, 2021 Camera-ready: July 8, 2021 Workshop: July 18 or 19 (TBA), 2021 Deadlines are Anywhere on Earth: https://en.wikipedia.org/wiki/Anywhere_on_Earth -------------------------------- -------------------------------- TOPICS OF INTEREST -------------------------------- Blockchains are decentralized transactional ledgers that rely on cryptographic hash functions for guaranteeing the integrity of the stored data. Participants on the network reach agreement on what valid transactions are through consensus algorithms. Blockchains may also provide support for Smart Contracts. Smart Contracts are scripts of an ad-hoc programming language that are stored in the Blockchain and that run on the network. They can interact with the ledger’s data and update its state. These scripts can express the logic of possibly complex contracts between users of the Blockchain. Thus, Smart Contracts can facilitate the economic activity of Blockchain participants. With the emergence and increasing popularity of cryptocurrencies such as Bitcoin and Ethereum, it is now of utmost importance to have strong guarantees of the behavior of Blockchain software. These guarantees can be brought by using Formal Methods. Indeed, Blockchain software encompasses many topics of computer science where using Formal Methods techniques and tools are relevant: consensus algorithms to ensure the liveness and the security of the data on the chain, programming languages specifically designed to write Smart Contracts, cryptographic protocols, such as zero-knowledge proofs, used to ensure privacy, etc. This workshop is a forum to identify theoretical and practical approaches of formal methods for Blockchain technology. Topics include, but are not limited to: * Formal models of Blockchain applications or concepts * Formal methods for consensus protocols * Formal methods for Blockchain-specific cryptographic primitives or protocols * Design and implementation of Smart Contract languages * Verification of Smart Contracts -------------------------------- -------------------------------- SUBMISSION -------------------------------- Submit original manuscripts (not published or considered elsewhere) with a page limit of 12 pages for full papers and 6 pages for short papers (excluding bibliography and short appendix of up to 5 additional pages). Alternatively you may also submit an extended abstract of up to 3 pages (including bibliography) summarizing your ongoing work in the area of formal methods and blockchain. Authors of selected extended-abstracts are invited to give a short lightning talk. Submission link: https://easychair.org/conferences/?conf=fmbc2021 Authors are encouraged to use LaTeX and prepare their submissions according to the instructions and styling guides for OASIcs provided by Dagstuhl. Instructions for authors: https://submission.dagstuhl.de/documentation/authors#oasics At least one author of an accepted paper is expected to present the paper at the workshop as a registered participant. -------------------------------- -------------------------------- PROCEEDINGS -------------------------------- All submissions will be peer-reviewed by at least three members of the program committee for quality and relevance. Accepted regular papers (full and short papers) will be included in the workshop proceedings, published as a volume of the OpenAccess Series in Informatics (OASIcs) by Dagstuhl. -------------------------------- -------------------------------- INVITED SPEAKER -------------------------------- David Dill, Lead Researcher, Blockchain, Novi/Facebook, USA https://research.fb.com/people/dill-david/ -------------------------------- -------------------------------- PROGRAM COMMITTEE -------------------------------- PC CO-CHAIRS * Bruno Bernardo (Nomadic Labs, France) (bruno(a)nomadic-labs.com) * Diego Marmsoler (University of Exeter, UK) (D.Marmsoler(a)exeter.ac.uk) PC MEMBERS * Wolfgang Ahrendt (Chalmers University of Technology, Sweden) * Lacramioara Astefanoei (Nomadic Labs, France) * Massimo Bartoletti (University of Cagliari, Italy) * Joachim Breitner (Dfinity Foundation, Germany) * Achim Brucker (University of Exeter, UK) * Zaynah Dargaye (Nomadic Labs, France) * Jérémie Decouchant (TU Delft, Netherlands) * Dana Drachsler Cohen (Technion, Israel) * Ansgar Fehnker (University of Twente, Netherlands) * Maurice Herlihy (Brown University, USA) * Lars Hupel (INNOQ, Germany) * Florian Kammueller (Middlesex University London, UK) * Igor Konnov (Informal Systems, Austria) * Andreas Lochbihler (Digital Asset, Switzerland) * Simão Melo de Sousa (Universidade da Beira Interior, Portugal) * Karl Palmskog (KTH, Sweden) * Maria Potop-Butucaru (Sorbonne Université, France) * Andreas Rossberg (Dfinity Foundation, Germany) * César Sanchez (Imdea, Spain) * Clara Schneidewind (TU Wien, Austria) * Ilya Sergey (Yale-NUS College/NUS, Singapore) * Mark Staples (CSIRO Data61, Australia) * Meng Sun (Peking University, China) * Simon Thompson (University of Kent, UK) * Josef Widder (Informal Systems, Austria)

1 0

ML Family Workshop 2021: first call for short abstracts and presentations
by Jonathan Protzenko 10 Apr '21

10 Apr '21

(tl;dr) The ML family workshop is back, and will be held virtually along with ICFP 2021. The workshop does not have proceedings, making it the perfect venue to run some ideas with the community or present some work in progress within a friendly environment. The PC has a broad expertise and submissions are 3 pages long: when in doubt, just submit! (long version) We are happy to announce that the ML Family Workshop is back for its 2021 edition, which we will be held online on Thursday August 26th, in conjunction with ICFP 2021. The ML family workshop warmly welcomes submission touching on the programming languages traditionally seen as part of the "ML family" (Standard ML, OCaml, F#, CakeML, SML#, Manticore, MetaOCaml, etc.). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. We also encourage presentations from related languages (such as Haskell, Scala, Rust, Nemerle, Links, Koka, F*, Eff, ATS, etc), to exchange experience of further developing ML ideas. ## Submission details Submissions must be at most three pages long; see the full call for papers <https://icfp21.sigplan.org/home/mlfamilyworkshop-2021#Call-for-Presentations> for details. Submission site: https://ml21.hotcrp.com/ ## Important dates Thu, May 27th 2021 (AoE): submission deadline Thu, Jun 17th 2021 (AoE): author notification Thu, Aug 26th: workshop (time slots TBD) ## Program committee Danel Ahman (University of Ljubljana) Robert Atkey (University of Strathclyde) Frédéric Bour (Tarides) Ezgi Çiçek (Facebook London) Youyou Cong (Tokyo Institute of Technology) Richard A. Eisenberg (Tweag I/O) Martin Elsman (University of Copenhagen, Denmark) Ohad Kammar (University of Edinburgh) Naoki Kobayashi (University of Tokyo, Japan) Benoît Montagu (Inria) Jonathan Protzenko (Microsoft Research) (Chair) Kristina Sojakova (INRIA Paris) Don Syme (Microsoft) Matías Toro (University of Chile) Katsuhiro Ueno (Tohoku University)

1 0

haskell text://protocol client?
by Petite Abeille 10 Apr '21

10 Apr '21

Hello, Would you know of any haskell text://protocol clients? Or servers? [1][2][3] Thanks in advance. [1] https://textprotocol.org [2] https://github.com/textprotocol/public [3] https://github.com/textprotocol/publictext

3 4

Haskell Joke of the Year 2020
by Nick Rudnick 09 Apr '21

09 Apr '21

Dear all, recently, I was confronted with a question what the Haskell joke of the year 2020 is – for anybody else, whose attention, like mine, this slipped completely, here it is, since it really is quite a bit funny, Haskellers don't make money… :-/ If anybody knows jokes of the other years, I'd be happy to know those, too! Cheers, and thanks in advance, Nick

1 0

Z.Haskell project announced
by Dong Han 07 Apr '21

07 Apr '21

Dear Haskellers: After having a discussion with HF guys, I decide to announce [Z.Haskell]( http://z.haskell.world/) project, It's available on Hackage and very much usable now, the document is also pretty adequate. To recap the document from Z.Haskell, Z.Haskell provides: + Array, vector(array slice), sorting, searching + Text based UTF-8, basic Unicode manipulating, regex + FFI utilities + Fast parsing and building monad + JSON encoding and decoding + IO resource management, resource pool + File system operations + Network: DNS, TCP, UDP and IPC + Buffered input and output + Process management + Environment settings + High performance logger + High performance low-resolution timer The project's goal is not to compete with the base, but to provide an alternative engineering toolkit, which is more suitable for writing practical network/storage services. Similar to [netty](https://netty.io/) for java or [nodejs](https://nodejs.org/) for javascript. Welcome to join Z.Haskell if you have a similar use case. Currently, we're heading with the following roadmap: + Crypto library based on [botan](https://github.com/ZHaskell/z-botan). + TLS network stack. + HTTP framework. + Distributed system algorithms. Happy hacking! Z.Haskell Contributors

2 2

Get proof of injectivity for an injective type family
by Andreas Källberg 07 Apr '21

07 Apr '21

Is there any way to get hold of a proof of injectivity for an injective type family? In other words, given this type family type family F a = b | b -> a can I get the term fInj :: F a ~ F b => (a ~ b => r) -> r in any way (without using unsafeCoerce)?

3 2

[ANN] aws-arn-0.1.0.0 - Library and optics for munging Amazon Resource Names (ARNs)
by Jack Kelly 07 Apr '21

07 Apr '21

I have just pushed an initial release of aws-arn[1] to Hackage. This library provides a type representing Amazon Resource Names (ARNs)[2], and parsing/unparsing functions for them. The provided optics make it very convenient to rewrite parts of ARNs. An example, from the documentation: API Gateway Lambda Authorizers are given the ARN of the requested endpoint and method, and are expected to respond with an IAM Policy Document. It is sometimes useful to manipulate the given ARN when describing which resources to authorize: -- Returns "arn:aws:execute-api:us-east-1:123456789012:my-spiffy-api/stage/*" let authorizerSampleARN = "arn:aws:execute-api:us-east-1:123456789012:my-spiffy-api/stage/GET/some/deep/path" in over (_ARN . arnResource . slashes) (\parts -> take 2 parts ++ ["*"]) authorizerSampleARN The code is available on GitHub[3]; bug reports and pull requests are welcome. There is some additional support for parsing specific resource types -- PRs to support more resource types are especially welcome. Best, -- Jack [1]: https://hackage.haskell.org/package/aws-arn-0.1.0.0 [2]: https://docs.aws.amazon.com/general/latest/gr/aws-arns-and-namespaces.html [3]: https://github.com/bellroy/aws-arn

1 0

Looking for a toy imperative language implementation in Haskell for research
by Igor Moreno Santos 07 Apr '21

07 Apr '21

Hi, I'm looking for a toy imperative language implementation in Haskell for research purposes. I imagine something like the language of arithmetic expressions from TAPL ch. 3 augmented with - while-loop (so the CFG has loops) - blocks (sequence of statements to put inside loops and conditionals) - assignment (otherwise we can't show any effects from sequences) I think there's probably nothing exactly like that so we might end up doing it ourselves but maybe there's already something out there. Thank you in advance. Regards, Igor Moreno

7 6

A functor for two Peano systems
by Galaxy Being 07 Apr '21

07 Apr '21

I'm just not understanding the concept of a functor in this context: I have this plus :: Int -> Int -> Int plus n m = if (n == 0) then m else sCessor (plus (pCessor n) m) where sCessor x = x + 1 pCessor x = if (x == 0) then error "too small" else (x - 1) and this data MyNum = MNZero | OneMoreThan MyNum deriving (Show,Eq,Ord) plus2 :: MyNum -> MyNum -> MyNum plus2 n m = if (n == MNZero) then m else sCessor (plus2 (pCessor n) m) where sCessor x = (OneMoreThan x) pCessor x = if (x == MNZero) then (error "too small") else (oneLess x) oneLess MNZero = MNZero oneLess (OneMoreThan myn) = myn It seems there should be just one plus, function that would handle both an Int-based Peano and the MyNum-based Peano, not two. But in this definition fmap :: (a -> b) -> f a -> f b The (a -> b) should be "lifted" over the f a -> f b But I can't conceive of how this should all fit together, i.e., to create just one generic plus that would handle both the plus :: Int -> Int -> Int and the plus2 :: MyNum -> MyNum -> MyNum. Trying to get started, I would assume I need some sort of instance Functor MyNum describing, yeah, what? Or am I barking up the completely wrong tree here, i.e., this isn't a functor issue? LB

3 3

How to ensure optimization for large immutable vectors to be shared w.r.t. Referential Transparency
by YueCompl 06 Apr '21

06 Apr '21

Hello Cafe and respected GHC Devs, I would like to ensure some immutable vectors (can be quite large) are always shared instead of copied, and I think that should be straight forward w.r.t. referential transparency we enjoy. In an attempt to determine whether two immutable vectors can be treated as the same one to enable specific optimizations for that case, I tried to use ST to determine their respective backing foreign ptrs for comparison. But appears it can be copied when wrapped in a newtype, I wonder why it is the case, and how to avoid the copy? Here's my minimum reproducible snippet: ```hs λ> :set -XBangPatterns λ> λ> :set -package vector package flags have changed, resetting and loading new packages... λ> λ> import Prelude λ> λ> import Control.Monad.ST λ> import qualified Data.Vector.Storable as VS λ> λ> :{ λ| λ| newtype SomeVector = SomeVector (VS.Vector Int) λ| λ| isSameVector :: SomeVector -> SomeVector -> Bool λ| isSameVector (SomeVector !x) (SomeVector !y) = runST $ do λ| mx(a)(VS.MVector !x'offset !x'fp) <- VS.unsafeThaw x λ| my(a)(VS.MVector !y'offset !y'fp) <- VS.unsafeThaw y λ| _ <- VS.unsafeFreeze mx λ| _ <- VS.unsafeFreeze my λ| return $ x'offset == y'offset && x'fp == y'fp λ| λ| :} λ> λ> let !v = VS.fromList [3,2,5] in isSameVector (SomeVector v) (SomeVector v) False λ> λ> let !v = SomeVector (VS.fromList [3,2,5]) in isSameVector v v True λ> ``` Thanks with best regards, Compl

3 10