Computational Logic SeminarTuesday, October 29, 20132:00 pmGraduate Center, rm. 3209

# J-Calc: Justified Modal Types and Functional Programs

## Konstantinos Pouliasis

### 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 by

on October 29th, 2013