Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

8.1K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0

#haskell

40 posts17 participants4 posts today
Jacket

#Functional programing will probably become the most popular paradigm of #quantum computing. It's impossible for now to copy a qubit so any algorithms has to be written in a stateless way. At the moment, quantum algorithms are written in a more declarative manner cause we are still figuring out how to do anything with those machine. There is some attempts at creating functional languages for quantum computers but at the moment you can't run them on hardware. I'm talking here about #Quipper, #QML, and #Silq but I'm convinced that this will be the way once we will figure out how to make a quantum computer stable. Quipper is based on #Haskell. I just find it cool.

José A. Alonso

Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. link.springer.com/article/10.1 #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming

SpringerLinkFormally Verified Suffix Array Construction - Journal of Automated ReasoningSuffix arrays are a data structure with numerous real-world applications. They are extensively used in text retrieval and data compression applications, including query suggestion mechanisms in web search, and in bioinformatics tools for DNA sequencing and matching. This wide applicability means that algorithms for constructing suffix arrays are of great practical importance. The SA-IS algorithm is an efficient but conceptually complex suffix array construction technique, and implementing it requires a deep understanding of its underlying theory. As a critical step towards developing a provably correct and efficient implementation, we have developed the SA-IS algorithm in Isabelle/HOL and formally verified that it is equivalent to a mathematical functional specification of suffix arrays, a task that required verifying a wide range of underlying properties of strings and suffixes. We also used Isabelle’s code extraction facilities to extract an executable Haskell implementation of SA-IS, which albeit is inefficient due to using lists and natural numbers rather than arrays and machine words, demonstrates that our verified HOL implementation of SA-IS can be refined to an executable implementation in its current form.
TrendingLive feeds
About