projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2014-03-04
Claudio Sacerdoti...
Different behaviour of OCaml 4.0.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-03
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-03-03
Ferruccio Guidi
some additions for the forthcoming presentation
commit
|
commitdiff
|
tree
|
snapshot
2014-02-28
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-28
Ferruccio Guidi
- some corrections and additions
commit
|
commitdiff
|
tree
|
snapshot
2014-02-27
Claudio Sacerdoti...
Porting of HOTT from Coq to Matita.
commit
|
commitdiff
|
tree
|
snapshot
2014-02-25
Ferruccio Guidi
relabelled documantation entries
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Ferruccio Guidi
update in web site and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Ferruccio Guidi
- we bypassed another false conjecture :) ...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
addition of unused material :)
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
update in ground_2 and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
a wrong conjecture bypassed!
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Ferruccio Guidi
update in basic_2 and ground_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Ferruccio Guidi
- main proposition on lsx finally proved!
commit
|
commitdiff
|
tree
|
snapshot
2014-02-18
Ferruccio Guidi
- a reinforement in a lemma on ldrop allows to prove...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-16
Ferruccio Guidi
- improved definition of lsx allows more invariants
commit
|
commitdiff
|
tree
|
snapshot
2014-02-11
Ferruccio Guidi
update in basic_2 and ground_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-11
Ferruccio Guidi
some advances on reduction
commit
|
commitdiff
|
tree
|
snapshot
2014-02-04
Ferruccio Guidi
evaluation for context-sensitive extended substitution...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Ferruccio Guidi
we start total substitution ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-31
Ferruccio Guidi
some notation renamed and fixed
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Ferruccio Guidi
normal forms for extended substitution
commit
|
commitdiff
|
tree
|
snapshot
2014-01-29
Ferruccio Guidi
bug fix in the notation of normal forms, now we specify...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Andrea Asperti
Almost there
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Andrea Asperti
progress
commit
|
commitdiff
|
tree
|
snapshot
2014-01-27
Ferruccio Guidi
some corrections ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-27
Andrea Asperti
working version
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Ferruccio Guidi
nat: we added a non-indexed theorem
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Andrea Asperti
more auxiliary machines
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Ferruccio Guidi
- nat: some additions, plus_minus_commutative renamed...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-20
Ferruccio Guidi
milestone in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-01-20
Ferruccio Guidi
commit completed: now we support two versions of slicin...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-18
Ferruccio Guidi
- commit of the "reduction" component with two addition...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
commit of the "unfold" component ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
commit of the "static" component
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
- commit of the "substitution" component
commit
|
commitdiff
|
tree
|
snapshot
2014-01-16
Ferruccio Guidi
commit of the "relocation" component with the new defin...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-15
Ferruccio Guidi
we start a criterion on extended computation
commit
|
commitdiff
|
tree
|
snapshot
2014-01-13
Ferruccio Guidi
some improvements on the relation lsx ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-10
Ferruccio Guidi
update in ground_2 and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-01-10
Ferruccio Guidi
new definition of lleq allows to complete the proof...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-09
Ferruccio Guidi
- ynat: some additions
commit
|
commitdiff
|
tree
|
snapshot
2014-01-06
Ferruccio Guidi
one file was missing :)
commit
|
commitdiff
|
tree
|
snapshot
2014-01-06
Ferruccio Guidi
- lleq now uses ynat
commit
|
commitdiff
|
tree
|
snapshot
2014-01-05
Ferruccio Guidi
- new definition of lazy equivalence for local environm...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-03
Ferruccio Guidi
- extended multiple substitutions now uses bounds in...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-03
Ferruccio Guidi
more arithmetics for natural numbers with infinity ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-28
Ferruccio Guidi
some improvements and new lemmas for
commit
|
commitdiff
|
tree
|
snapshot
2013-12-26
Ferruccio Guidi
the theory of extended multiple substitution for therms...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-20
Ferruccio Guidi
theory of extended iterated substitution begins ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-19
Ferruccio Guidi
theory of cpy is complete!
commit
|
commitdiff
|
tree
|
snapshot
2013-12-19
Ferruccio Guidi
the theory of cpy continues ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-17
Ferruccio Guidi
refinement for extended substitution completed
commit
|
commitdiff
|
tree
|
snapshot
2013-12-16
Ferruccio Guidi
- lsubr moved down one component
commit
|
commitdiff
|
tree
|
snapshot
2013-12-15
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-15
Ferruccio Guidi
eliminators of arited terms based on "big tree" proper...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-14
Ferruccio Guidi
update in basic_2 completed
commit
|
commitdiff
|
tree
|
snapshot
2013-12-14
Ferruccio Guidi
one file was still missing
commit
|
commitdiff
|
tree
|
snapshot
2013-12-14
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-14
Ferruccio Guidi
commit is now complete :)
commit
|
commitdiff
|
tree
|
snapshot
2013-12-14
Ferruccio Guidi
- "big tree" theorem is now proved up to some conjectur...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-09
Ferruccio Guidi
- first results on strongly normalizing local environments
commit
|
commitdiff
|
tree
|
snapshot
2013-12-06
Ferruccio Guidi
partial commit ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-04
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-04
Ferruccio Guidi
third commutation property on lazy equivalence for
commit
|
commitdiff
|
tree
|
snapshot
2013-12-04
Andrea Asperti
New approach: we use "iterator" steps in place of pointers.
commit
|
commitdiff
|
tree
|
snapshot
2013-12-04
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-04
Ferruccio Guidi
first and second commutation property on lazy equivalen...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Claudio Sacerdoti...
1. more bugs fixed
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Ferruccio Guidi
- last patrtial commit of the "reduction" and "computat...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Claudio Sacerdoti...
More progress.
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Claudio Sacerdoti...
Some progress in the correctness proof and a bug fixed.
commit
|
commitdiff
|
tree
|
snapshot
2013-12-02
Ferruccio Guidi
initial commit of the "rduction" component
commit
|
commitdiff
|
tree
|
snapshot
2013-12-01
Ferruccio Guidi
update in ground_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-01
Ferruccio Guidi
commit of the "substitution" component and of some...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-01
Ferruccio Guidi
- improved arithmetics for natural numbers with infinity
commit
|
commitdiff
|
tree
|
snapshot
2013-11-29
Andrea Asperti
A first example that uses a status monad where the...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-29
Ferruccio Guidi
addition for natural numbers with infinity
commit
|
commitdiff
|
tree
|
snapshot
2013-11-28
Ferruccio Guidi
update in ground_2, web page for ground_2
commit
|
commitdiff
|
tree
|
snapshot
2013-11-28
Ferruccio Guidi
definition of equivalence for local environments,
commit
|
commitdiff
|
tree
|
snapshot
2013-11-27
Ferruccio Guidi
web page for ground_2 and bugfixed statistics generatio...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-27
Ferruccio Guidi
strict order relation for natural numbers with inifinity
commit
|
commitdiff
|
tree
|
snapshot
2013-11-26
Ferruccio Guidi
- natural numbers with infinity for lambdadelta
commit
|
commitdiff
|
tree
|
snapshot
2013-11-25
Ferruccio Guidi
update in ground_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-25
Ferruccio Guidi
- xoa: the definitions file now includes the notations...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-15
Wilmer Ricciotti
Final version of the binary machine (all proofs completed).
commit
|
commitdiff
|
tree
|
snapshot
2013-11-07
Wilmer Ricciotti
Closes many daemons.
commit
|
commitdiff
|
tree
|
snapshot
2013-11-06
Wilmer Ricciotti
Full rework of the semantics of the binary machine...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-03
Wilmer Ricciotti
Almost finished...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-03
Wilmer Ricciotti
Major bugfix/reorganization/improvement of the partial...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-03
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-11-03
Ferruccio Guidi
second and third commutation property on lazy equivalen...
commit
|
commitdiff
|
tree
|
snapshot
2013-11-01
Ferruccio Guidi
update in basic_2 (bugfix)
commit
|
commitdiff
|
tree
|
snapshot
2013-11-01
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-11-01
Ferruccio Guidi
- lambdadelta: first commutation property on lazy equiv...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-28
Ferruccio Guidi
lazy equivalence for local environments is now defined
commit
|
commitdiff
|
tree
|
snapshot
2013-10-28
Andrea Asperti
Splitted star
commit
|
commitdiff
|
tree
|
snapshot
2013-10-27
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-27
Ferruccio Guidi
- lambdadelta: tentative definition of lazy equivalence...
commit
|
commitdiff
|
tree
|
snapshot
next