On-device research index

arXiv research

A locally-built, LLM-digested index of recent arXiv papers in quant finance, geometry/topology, and statistical ML — keyword search served straight from SQLite on this machine.

168,657 papers · 148 categories

Trend · papers per month

count % of corpus

2 results for “OCaml”

Double Auctions: Formalization and Automated Checkerscs.LO

We formalize and verify double auctions for multiple-quantity trades.

problem Matching multiple-quantity trade requests in double auctions.

method Formalized algorithms, correctness proofs, Coq proof assistant, verified OCaml and Haskell programs.

result Automatic detection of violations in exchange systems.

double auctions formal verification Coq OCaml Haskell

2024-10-24abs ↗pdf ↗

Efficient and Verified Continuous Double Auctionscs.LO

Efficient verified double auctions improve matching speed and detect errors.

problem Improving the efficiency and reliability of double auctions in financial markets.

method Formally verified implementation using Coq proof assistant, reducing time complexity and improving error detection.

result Improved efficiency with

O(n \log n)

time complexity, reducing runtime from days to minutes.

double auctions formal verification Coq proof assistant error detection time complexity

2024-12-11abs ↗pdf ↗