Email Gateway (Aug 19 2022 at 14:19): Email Gateway (Aug 19 2022 at 14:19):From: Lawrence Paulson <lp15@cam.ac.uk>
A shallow embedding of HyperCTL*
by Markus N. Rabe, Peter Lammich and Andrei Popescu
We formalize HyperCTL, a temporal logic for expressing security properties. We first define a shallow embedding of HyperCTL, within which we prove inductive and coinductive rules for the operators. Then we show that a HyperCTL* formula captures Goguen-Meseguer noninterference, a landmark information flow property. We also define a deep embedding and connect it to the shallow embedding by a denotational semantics, for which we prove sanity w.r.t. dependence on the free variables. Finally, we show that under some finiteness assumptions about the model, noninterference is given by a (finitary) syntactic formula.
http://afp.sourceforge.net/entries/HyperCTL.shtml
Abstract Completeness
by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel
A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the first-order logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL---e.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instance---many-sorted FOL with equality---is described elsewhere [Blanchette and Popescu, FroCoS 2013].
http://afp.sourceforge.net/entries/Abstract_Completeness.shtml
Contributions are coming in thick and fast these days.
Larry Paulson
Email Gateway (Aug 22 2022 at 15:15):From: Gerwin.Klein@data61.csiro.au
New at https://isa-afp.org:
Lower bound on comparison-based sorting algorithms
by Manuel Eberl
This article contains a formal proof of the well-known fact that number of comparisons that a comparison-based sorting algorithm needs to perform to sort a list of length n is at least log2 (n!) in the worst case, i. e. Ω(n log n).
For this purpose, a shallow embedding for comparison-based sorting algorithms is defined: a sorting algorithm is a recursive datatype containing either a HOL function or a query of a comparison oracle with a continuation containing the remaining computation. This makes it possible to force the algorithm to use only comparisons and to track the number of comparisons made.
The number of comparisons in QuickSort
by Manuel Eberl
We give a formal proof of the well-known results about the number of comparisons performed by two variants of QuickSort: first, the expected number of comparisons of randomised QuickSort (i. e. QuickSort with random pivot choice) is 2 (n+1) H_n - 4 n, which is asymptotically equivalent to 2 n ln n; second, the number of comparisons performed by the classic non-randomised QuickSort has the same distribution in the average case as the randomised one.
Enjoy!
Gerwin
Email Gateway (Aug 22 2022 at 15:15):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
I find “New in the AFP: …” subjects much more helpful than
“$n$ new AFP entries”, and it seems to be a bit unfair that some AFP
entries get less promotion just because they happen to be accepted
together with others. Why not announce each entry individually? I think
nobody would mind the few extra mails.
Greetings from Philly,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 15:15):From: Max Haslbeck <max.haslbeck@gmx.de>
Hi,
I just wanted to add that there's now an RSS feed which you can follow
for updates on new entries:
<https://www.isa-afp.org/rss.xml>
Gruß
Max
Email Gateway (Aug 22 2022 at 15:16):From: Gerwin.Klein@data61.csiro.au
And a twitter account @isaprover ;-)
I do take the point, though, that it slightly decreases exposure for multiple entries (these two by the same author).
Cheers,
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC