
Programming in constructive type theory corresponds to theorem proving in mathematics: the specification plays the role of the proposition to be proved and the program is obtained from the proof. In this paper, we present an approach of using constructive type theory to derive a debugger of a given programming language from its denotational semantic definition. The development is supported by a proof development system called PowerEpsilon .
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
