Analysis and synthesis of inductive families
<p>Based on a natural unification of logic and computation, Martin-Löf’s <em>intuitionistic type theory</em> can be regarded simultaneously as a computationally meaningful higher-order logic system and an expressively typed functional programming language, in which proofs and progr...
| Автор: | |
|---|---|
| Інші автори: | |
| Формат: | Дисертація |
| Мова: | English |
| Опубліковано: |
2014
|