31 citations · 76 across the 9 of their papers we have counts for
5 papers · 1 filter
A Formalization of SQL with Nulls
Wilmer Ricciotti, James Cheney
SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is base…
Explicit Auditing
Wilmer Ricciotti, James Cheney
The Calculus of Audited Units (CAU) is a typed lambda calculus resulting from a computational interpretation of Artemov's Justification Logic under the Curry-Howard isomorphism; it…
Strongly Normalizing Audited Computation
Wilmer Ricciotti, James Cheney
Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and ac…
A Web Interface for Matita
Andrea Asperti, Wilmer Ricciotti
This article describes a prototype implementation of a web interface for the Matita proof assistant. The interface supports all basic functionalities of the local Gtk interface, bu…
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen +1
The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is…