Data Science (DaS) Research Publications

2014 2013 2009 2008


Lionel Elie Mamane, Herman Geuvers, and James McKinna. A Saturated Extension of Lambda-Bar-Mu-Mu-Tilde. Technical report: ICIS-R09002, July, Radboud University Nijmegen, 2009.

This report presents a proof language based on the work of Sacerdoti Coen, Kirchner and Autexier on lambda-bar-mu-mu-tilde,a calculus introduced by Curien and Herbelin. Just as lambda-bar-mu-mu-tilde preserves several proof structures that are identified by the lambda-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being /logically saturated/. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses. We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar. lambda-bar-mu-mu-tilde is a proof term language for sequent calculus proofs; the pseudo-natural language rendering thus contributes a way to talk about these proofs in natural language.

[ PDF ] [ Bibtex ] [ External URL ]

Milad Niqui, and Freek Wiedijk. `Many Digits` Friendly Competition. Technical report: ICIS-R09007, December, Radboud University Nijmegen, 2009.

In this article we give an account of the ``Many Digits`` friendly competition, a competition between arbitrary precision arithmetic packages that was organised following the competition described in J. Blanck, ``Exact Real Arithmetic Systems: Results of Competition``, and was held on October 3-4, 2005 in order to investigate the state of the art in the field of exact and arbitrary precision arithmetic. The competition consisted of two types of problems, a basic and an intermediate set. The basic problems consisted of simple expressions involving elementary functions. The intermediate problems involved more mathematical construct or slightly more programming. A solution consisted of a sequence of decimal digits, for most problems 10000 digits. The systems were required to calculate the solution within two minutes and depending on their success retry the problem with a higher/lower number of digits. The competition had nine participants, some of them competing remotely.

[ PDF ] [ Bibtex ]