Zobrazeno 1 - 10
of 177
pro vyhledávání: '"O'Connor, Russell"'
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
To build a large library of mathematics, it seems more efficient to take advantage of the inherent structure of mathematical theories. Various theory presentation combinators have been proposed, and some have been implemented, in both legacy and curr
Externí odkaz:
http://arxiv.org/abs/1812.08079
Autor:
O'Connor, Russell
Publikováno v:
2017. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. ACM, New York, NY, USA
Simplicity is a typed, combinator-based, functional language without loops and recursion, designed to be used for crypto-currencies and blockchain applications. It aims to improve upon existing crypto-currency languages, such as Bitcoin Script and Et
Externí odkaz:
http://arxiv.org/abs/1711.03028
Kniha
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Jaskelioff, Mauro, O'Connor, Russell
Representation theorems relate seemingly complex objects to concrete, more tractable ones. In this paper, we take advantage of the abstraction power of category theory and provide a general representation theorem for a wide class of second-order func
Externí odkaz:
http://arxiv.org/abs/1402.1699
Autor:
Carette, Jacques, O'Connor, Russell
Publikováno v:
AISC/MKM/Calculemus 2012: 202-215
We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category of contexts and fibered categories are the ideal theoretical tools for
Externí odkaz:
http://arxiv.org/abs/1204.0053
Autor:
Carette, Jacques, Farmer, William M., Jeremic, Filip, Maccio, Vincent, O'Connor, Russell, Tran, Quang M.
We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for our library design to use and reflect, as much as possible, the mathema
Externí odkaz:
http://arxiv.org/abs/1106.1862
Autor:
O'Connor, Russell
This paper gives two new categorical characterisations of lenses: one as a coalgebra of the store comonad, and the other as a monoidal natural transformation on a category of a certain class of coalgebras. The store comonad of the first characterisat
Externí odkaz:
http://arxiv.org/abs/1103.2841
Autor:
O'Connor, Russell
Publikováno v:
Mathematical Structures in Computer Science (2011), 21: 861-882
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported
Externí odkaz:
http://arxiv.org/abs/1008.1213
Autor:
Kaliszyk, Cezary, O'Connor, Russell
Publikováno v:
Journal of Formalized Reasoning, 2(1):27-39, 2009
There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN library from Nijmegen defines constructively valid real numbers. Unfortun
Externí odkaz:
http://arxiv.org/abs/0809.1644