 25 Jun, 2018 1 commit


Ralf Jung authored

 27 Apr, 2018 1 commit


Robbert Krebbers authored

 12 Jan, 2018 1 commit


Robbert Krebbers authored

 09 Nov, 2017 1 commit


Robbert Krebbers authored

 01 Nov, 2017 1 commit


Johannes Kloos authored
This generalizes Fix_unfold to a setoid setting. In particular, we can use this to unfold multiargument fixpoints without requiring functional extensionality.

 24 Sep, 2017 1 commit


Robbert Krebbers authored

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 14 Mar, 2017 1 commit


Ralf Jung authored

 31 Jan, 2017 3 commits


Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored
This patch was created using find name *.v  xargs L 1 awk i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing

 17 Nov, 2016 1 commit


Robbert Krebbers authored

 16 Nov, 2016 1 commit


Robbert Krebbers authored

 20 Feb, 2016 1 commit


Ralf Jung authored

 17 Feb, 2016 1 commit


Robbert Krebbers authored

 13 Feb, 2016 1 commit


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.

 16 Nov, 2015 1 commit


Robbert Krebbers authored

 03 Feb, 2017 1 commit


Robbert Krebbers authored

 22 Apr, 2015 1 commit


Robbert Krebbers authored

 08 Feb, 2015 1 commit


Robbert Krebbers authored

 10 Oct, 2014 1 commit


Robbert Krebbers authored
The proof now uses the stronger notion of memory permutation instead of a more general memory refinement. We have also proven that memory permutations are symmetric.

 03 Oct, 2014 1 commit


Robbert Krebbers authored
Also better error messages if a constant expression is expected.

 06 Sep, 2014 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 02 May, 2014 1 commit


Robbert Krebbers authored

 17 Jun, 2013 1 commit


Robbert Krebbers authored

 19 Feb, 2013 1 commit


Robbert Krebbers authored
Both the operational and axiomatic semantics are extended with sequence points and a permission system based on fractional permissions. In order to achieve this, the memory model has been completely revised, and is now built on top of an abstract interface for permissions. Apart from these changed, the library on lists and sets has been heavily extended, and minor changed have been made to other parts of the prelude.

 09 Jan, 2013 1 commit


Robbert Krebbers authored
The development now corresponds exactly to the FoSSaCS 2013 paper. Also, the prelude is updated to the one of the master branch.

 05 Jan, 2013 1 commit


Robbert Krebbers authored
* Define the standard strict order on pre orders. * Prove that this strict order is well founded for finite sets and finite maps. We also provide some utilities to compute with well founded recursion. * Improve the "simplify_option_equality" tactic to handle more cases. * Axiomatize finiteness of finite maps by translation to lists, instead of by them having a finite domain. * Prove many additional properties of finite maps. * Add many functions and theorems on lists, including: permutations, resize, filter, ...

 12 Nov, 2012 1 commit


Robbert Krebbers authored
Most interestingly: * Use [lia] instead of [omega] everywhere * More many generic lemmas on the memory to the theory on finite maps. * Many additional list lemmas. * A new interface for a monad for collections, which is now also used by the collection tactics. * Provide an additional finite collection implementation using unordered lists without duplicates removed. This implementation forms a monad (just the list monad in disguise).

 19 Oct, 2012 1 commit


Robbert Krebbers authored
The following things have been changed in this revision: * We now give a small step semantics for expressions. The denotational semantics only works for sideeffect free expressions. * Dynamically allocated memory through alloc and free is now supported. * The following expressions are added: assignment, function call, unary operators, conditional, alloc, and free. * Some customary induction schemes for expressions are proven. * The axiomatic semantics (and its interpretation) have been changed in order to deal with nondeterministic expressions. * We have added inversion schemes based on small inversions for the operational semantics. Inversions using these schemes are much faster. * We improved the statement preservation proof of the operational semantics. * We now use a variant of SsReflect's [by] and [done], instead of Coq's [now] and [easy]. The [done] tactic is much faster as it does not perform inversions. * Add theory, definitions and notations on vectors. * Separate theory on contexts. * Change [Arguments] declarations to ensure better unfolding.

 29 Aug, 2012 1 commit


Robbert Krebbers authored
improve some definitions, simplify some proofs.
