Computational Logic SeminarTuesday, October 29, 20132:00 pmGraduate Center, rm. 3209
J-Calc: Justified Modal Types and Functional Programs
Graduate Center CUNY
In this talk we give a computationally motivated presentation of J-Calc. J-Calc is an extension of simply typed lambda calculus with justifications and justified modal types.
Initiating from textbook examples of modular programs, we will present the modal type theory of J-Calc as a type system corresponding to programming with modular definitions. More specifically, we will show how justified modality offers a logical reading to separate compilation in modular functional programming.
Posted byon October 29th, 2013