31 citations · 76 across the 9 of their papers we have counts for
11 papers
Comprehending nulls
James Cheney, Wilmer Ricciotti
The Nested Relational Calculus (NRC) has been an influential high-level query language, providing power and flexibility while still allowing translation to standard SQL queries. It…
Query Lifting: Language-integrated query for heterogeneous nested collections
Wilmer Ricciotti, James Cheney
Language-integrated query based on comprehension syntax is a powerful technique for safe database programming, and provides a basis for advanced techniques such as query shredding…
Strongly-Normalizing Higher-Order Relational Queries
Wilmer Ricciotti, James Cheney
Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query t…
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…
Mixing set and bag semantics
Wilmer Ricciotti, James Cheney
The conservativity theorem for nested relational calculus implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relati…
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…
Imperative Functional Programs that Explain their Work
Wilmer Ricciotti, Jan Stolarek, Roly Perera +1
Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work by Perera et al., where dynami…
Abstracting an operational semantics to finite automata
Nadezhda Baklanova, Wilmer Ricciotti, Jan-Georg Smaus +1
There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction…
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…