projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2014-07-05
Ferruccio Guidi
improved example: Delta must be a family of terms
commit
|
commitdiff
|
tree
|
snapshot
2014-07-04
Ferruccio Guidi
- now unicode characters are counted :)
commit
|
commitdiff
|
tree
|
snapshot
2014-07-04
Ferruccio Guidi
important update in basic_2: cpr is not antisymmetric
commit
|
commitdiff
|
tree
|
snapshot
2014-07-04
Ferruccio Guidi
conjecture on antisymmetry of cpr finally closed
commit
|
commitdiff
|
tree
|
snapshot
2014-06-30
Ferruccio Guidi
some additions and corrections ...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-29
Ferruccio Guidi
- we begin the new site based on ld_web
commit
|
commitdiff
|
tree
|
snapshot
2014-06-29
Ferruccio Guidi
- wrong version of drop was used in four places
commit
|
commitdiff
|
tree
|
snapshot
2014-06-28
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-06-28
Ferruccio Guidi
- ldrop is now drop as in basic_1
commit
|
commitdiff
|
tree
|
snapshot
2014-06-25
Ferruccio Guidi
updated slides
commit
|
commitdiff
|
tree
|
snapshot
2014-06-25
Ferruccio Guidi
pathologic @-typing removed by adding imp-introduction
commit
|
commitdiff
|
tree
|
snapshot
2014-06-19
Ferruccio Guidi
misspelled filename :(
commit
|
commitdiff
|
tree
|
snapshot
2014-06-19
Ferruccio Guidi
milestone reported on web site
commit
|
commitdiff
|
tree
|
snapshot
2014-06-19
Ferruccio Guidi
- we upload communication #8
commit
|
commitdiff
|
tree
|
snapshot
2014-06-19
Ferruccio Guidi
- some pending conjectures closed in basic_2 and ground_2
commit
|
commitdiff
|
tree
|
snapshot
2014-06-18
Ferruccio Guidi
milestone in basic_2 !!
commit
|
commitdiff
|
tree
|
snapshot
2014-06-18
Ferruccio Guidi
milestone connit for preservation:
commit
|
commitdiff
|
tree
|
snapshot
2014-06-15
Ferruccio Guidi
minor update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-06-15
Ferruccio Guidi
- we introduce stratified term equivalence to remove...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-14
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-14
Ferruccio Guidi
reorganization of the "static" component:
commit
|
commitdiff
|
tree
|
snapshot
2014-06-10
Ferruccio Guidi
preservation of stratified vaildity through ordinary...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-10
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-09
Ferruccio Guidi
advances on append allow to complete the long awaited...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-09
Ferruccio Guidi
mailstone in basic_2 !! "big tree" theorem completed...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-08
Ferruccio Guidi
now we use the version of lazy union for local environm...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-08
Ferruccio Guidi
bug fix in lazy union for local environments
commit
|
commitdiff
|
tree
|
snapshot
2014-06-08
Ferruccio Guidi
- some work on append
commit
|
commitdiff
|
tree
|
snapshot
2014-06-07
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-07
Ferruccio Guidi
source table bugfixed
commit
|
commitdiff
|
tree
|
snapshot
2014-06-07
Ferruccio Guidi
- advances on free variables allow to reduce lleq_lpx_t...
commit
|
commitdiff
|
tree
|
snapshot
2014-06-01
Ferruccio Guidi
- some refactoring and minor additions
commit
|
commitdiff
|
tree
|
snapshot
2014-06-01
Ferruccio Guidi
- advances on hereditarily free variables: now "frees...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-26
Ferruccio Guidi
one file was missing :(
commit
|
commitdiff
|
tree
|
snapshot
2014-05-26
Ferruccio Guidi
new definition of llor gives a long awaited lemma :),
commit
|
commitdiff
|
tree
|
snapshot
2014-05-25
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-25
Ferruccio Guidi
- theory of llor now includes (long awaited) non-recurs...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-24
Ferruccio Guidi
non-recursive alternative of llpx_sn completed !
commit
|
commitdiff
|
tree
|
snapshot
2014-05-23
Ferruccio Guidi
update in grond_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-23
Ferruccio Guidi
advances on cofrees allows to prove one direction of
commit
|
commitdiff
|
tree
|
snapshot
2014-05-11
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-11
Ferruccio Guidi
advances on ldrop ....
commit
|
commitdiff
|
tree
|
snapshot
2014-05-10
Ferruccio Guidi
advances on cofrees
commit
|
commitdiff
|
tree
|
snapshot
2014-04-27
Ferruccio Guidi
reordering abstract computation properties and saturati...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-25
Ferruccio Guidi
one file was missing ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-25
Ferruccio Guidi
- advances in the theory of cofrees
commit
|
commitdiff
|
tree
|
snapshot
2014-04-21
Ferruccio Guidi
- we introduce recursive free variables of a term in...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-20
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-20
Ferruccio Guidi
- name changes in the rediction rules
commit
|
commitdiff
|
tree
|
snapshot
2014-04-18
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-18
Ferruccio Guidi
- the relation for pointwise extensions now takes a...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-16
Ferruccio Guidi
anniversary milestone in basic_2 !!
commit
|
commitdiff
|
tree
|
snapshot
2014-04-16
Ferruccio Guidi
3rd anniversary milestone
commit
|
commitdiff
|
tree
|
snapshot
2014-04-15
Ferruccio Guidi
- lazy extended reduction parked
commit
|
commitdiff
|
tree
|
snapshot
2014-04-13
Ferruccio Guidi
we restored the strong normalization of extended comput...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-10
Ferruccio Guidi
commit completed: one file was missing :(
commit
|
commitdiff
|
tree
|
snapshot
2014-04-10
Ferruccio Guidi
- some work on extensions:
commit
|
commitdiff
|
tree
|
snapshot
2014-04-08
Ferruccio Guidi
some advances on pointwise union for local environments ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-07
Ferruccio Guidi
some resuls on pointwise extensions (all of them are...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-05
Ferruccio Guidi
commit completed:
commit
|
commitdiff
|
tree
|
snapshot
2014-04-02
Ferruccio Guidi
commit of the "computation" component with lazy pointwi...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-30
Ferruccio Guidi
update of the partial commit:
commit
|
commitdiff
|
tree
|
snapshot
2014-03-25
Ferruccio Guidi
- partial commit: just the components below "computation"
commit
|
commitdiff
|
tree
|
snapshot
2014-03-20
Ferruccio Guidi
continuing on lazy pointwise extensions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-19
Ferruccio Guidi
we begin to develop lazy pointwisee extensions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-11
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-11
Ferruccio Guidi
reaxiomatized lleq fixes a bug in it and allows to...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Ferruccio Guidi
some additions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-08
Ferruccio Guidi
we define the lazy poinwise extension of a relation...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-08
Ferruccio Guidi
some corrections ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Code changed a bit to make it work as before with OCaml...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Do not assert false for a print not implemented yet.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Hocus-pocus code to use the old (and deprecated) implem...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Andrea Asperti
Minor changes to make the script more robust to strateg...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Ferruccio Guidi
some external links updated
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Ferruccio Guidi
a suggestion was added to avoid 1 pseudo reduction...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
Inclusions improved to allow compilation from the toplevel.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
Bug fixed: the tactic to analyze the term and understan...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
OCaml 4.0 detects a not handled case.
commit
|
commitdiff
|
tree
|
snapshot
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
next