projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
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
2013-10-26
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-26
Ferruccio Guidi
- bug fix in the connection between global and restrict...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-25
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-25
Ferruccio Guidi
- bug fix in the induction for the closure property
commit
|
commitdiff
|
tree
|
snapshot
2013-10-25
Andrea Asperti
full.ma
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Ferruccio Guidi
some additions needed for lambda_delta
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Ferruccio Guidi
- "small step" version of "big tree" theorem proved
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Andrea Asperti
step (almost) done
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Andrea Asperti
The step machine (draft)
commit
|
commitdiff
|
tree
|
snapshot
2013-10-24
Andrea Asperti
many changes
commit
|
commitdiff
|
tree
|
snapshot
2013-10-20
Wilmer Ricciotti
Completes all the phases of the binary machine (modulo...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-19
Ferruccio Guidi
more results towards the "big-tree" theorem ...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-19
Andrea Asperti
Slowly porting to an enriched tape alphabet
commit
|
commitdiff
|
tree
|
snapshot
2013-10-18
Andrea Asperti
The moves (almost)
commit
|
commitdiff
|
tree
|
snapshot
2013-10-15
Andrea Asperti
added sem_seq_app for the mono case
commit
|
commitdiff
|
tree
|
snapshot
2013-10-15
Andrea Asperti
renaming files
commit
|
commitdiff
|
tree
|
snapshot
2013-10-14
Ferruccio Guidi
strongly normalizing terms for big-tree reduction are...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-14
Andrea Asperti
almost there
commit
|
commitdiff
|
tree
|
snapshot
2013-10-14
Wilmer Ricciotti
Completed phases 0, 1, and 3.
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Ferruccio Guidi
some renaming ...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Andrea Asperti
Still a problem to be fixed: after reaching the border...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Andrea Asperti
shift a trace from an extremity
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Andrea Asperti
splitting files
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Andrea Asperti
Moved multi_to_mono.ma inside multi_to_mono
commit
|
commitdiff
|
tree
|
snapshot
2013-10-12
Andrea Asperti
Added a new directory for multi to mono
commit
|
commitdiff
|
tree
|
snapshot
2013-10-11
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-11
Ferruccio Guidi
bug fix in supclosure allows alternative definition...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-09
Wilmer Ricciotti
progress in the semantics of binary machines
commit
|
commitdiff
|
tree
|
snapshot
2013-10-08
Ferruccio Guidi
bugfix in possible alternative definition of fpbs
commit
|
commitdiff
|
tree
|
snapshot
2013-10-07
Ferruccio Guidi
some improvements towards an alternative definition...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-07
Wilmer Ricciotti
Starting proof about semantics of binary machines.
commit
|
commitdiff
|
tree
|
snapshot
2013-10-07
Wilmer Ricciotti
Completes the definition of binaryTM.
commit
|
commitdiff
|
tree
|
snapshot
2013-10-06
Andrea Asperti
progress in the deifinition of the semantics of the...
commit
|
commitdiff
|
tree
|
snapshot
2013-10-06
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-06
Ferruccio Guidi
bug fix in big-tree reduction
commit
|
commitdiff
|
tree
|
snapshot
2013-10-06
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-10-06
Ferruccio Guidi
- big-tree reduction is now based on extended reduction
commit
|
commitdiff
|
tree
|
snapshot
next