Deduction in Ramified Partial Type Theory: Focus on Derivation with Typing Judgements

Investor logo
Authors

RACLAVSKÝ Jiří

Year of publication 2016
Type Conference abstract
MU Faculty or unit

Faculty of Arts

Citation
Description In computer science, type theory is massively used as the basis of functional programming and theorem provers. Explicit use of typing judgements, e.g. ``$X$ is of type $\tau$.'', enables us a better control of programme behaviour (preventing cycling, ...), better control over quantification (preventing paradoxes, ...). The present talk focuses on deduction with typing judgements in Tichý's partial type theory, which is valuable because of its implementing partiality, incl. partiality of entities allowed in its ramified part.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.