[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 14.08.2012 11:13, Altenkirch Thorsten wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
An alternative are semantic methods, I.e. normalisation by evaluation.
There is a weak version for combinatory logic which can be used to only
implement beta reduction (but not xi or eta rules) or a strong one which
does give you full beta eta equality. However, to extend strong NBE for
more complex systems can be quite tricky too. I don't think I have seen a
straightforward extension of the strong version to dependent types (I am
saying this expecting somebody to scream :-).
Yes, me!
Towards Normalization by Evaluation for the Calculus of Constructions
Andreas Abel
Tenth International Symposium on Functional and Logic Programming,
FLOPS 2010, 19-21 April 2010, Sendai, Japan © Springer.
http://www2.tcs.ifi.lmu.de/~abel/publications.html#flops10
With computation on the type-level, it does not get much more
straightforward...
Cheers,
Andreas
Another idea which James Chapman and I have investigated is to directly
prove that the natural implementation of a decision procedure using big
step semantics is correct. This also has the advantage that you actually
prove the correctness of the implementation. This has been written up in
James PhD and there is also a journal paper - see
http://www.cs.nott.ac.uk/~txa/publ/jtait07.pdf
Cheers,
Thorsten
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
[email protected]
http://www2.tcs.ifi.lmu.de/~abel/
