Anonymous user
Talk:Proof: Difference between revisions
m
no edit summary
No edit summary |
mNo edit summary |
||
Line 13:
::: The issue is not about the use of metatheory but is about the use of programming. Currently, we have the Salmon implementation for the task, which does not correspond to code that I can run. More generally, the task requires no machine output. In my experience, the educational value of this site is significantly improved when short bits of machine output are included to illustrate the behavior of the code. --[[User:Rdm|Rdm]] 13:04, 31 May 2012 (UTC)
:::: But all the languages which are suitable for this task are based on some metatheories. Twelf is based on the [[wp:Logical_framework|LF]], Agda and Omega are based on the [[wp:Intuitionistic_type_theory|MLTT]], Coq is based on the [[wp:Calculus_of_constructions|CIC]] (which is variation of the MLTT),
:::: About the output, if the proof is correct, then there is nothing to report (or just report "
:::: I don't know about Salmon, but all you can do in C, J, Tcl or whatever is [http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf implement] dependently typed language or proof system, i.e. define syntax for terms and types (or terms, formulas and deduction rules) and write an unification algorithm on types and terms. — [[User:Ht|Ht]] 03:23, 1 June 2012 (UTC)
|