Seminari del Dipartimento

Logica e Informatica Teorica

Embedded programming style allows to split the syntax in two parts, representing respectively a host language H and a core language C embedded in H. This formally models several situations in which a user writes code in a main language and delegates some tasks to an ad hoc domain specific language. Moreover, as showed in recent years, a particular case of the host-core approach allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms such as quantum computing. The definition of a systematised type theory to capture and standardize common properties of embedded languages is partially unexplored. We present a flexible fragment of such a type theory, together with its semantics in terms of enriched categories. We introduce the calculus HC0 and we use the notion of internal language of a category to relate the language to the class of its models, showing the equivalence between the category of models and the one of theories. This provides a stronger result w.r.t. standard soundness and completeness since it involves not only the models but also morphisms between models. We observe that the definition of the morphisms between models highlights further advantages of the embedded languages and we discuss some concrete instances, extensions and specializations of the syntax and the semantics.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it
o cliccare sul seguente link Teams meeting: https://teams.microsoft.com/dl/launcher/launcher.html?url=%2f_%23%2fl%2fmeetup-join%2f19%3a388bb369590943489346c5edc8bb7b83%40thread.tacv2%2f1591225361019%3fcontext%3d%257B%2522Tid%2522%3a%2522ffb4df68-f464-458c-a546-00fb3af66f6a%2522%2c%2522Oid%2522%3a%252211647586-a255-4c31-b3ea-1a3032a3b0a8%2522%257D%26anon%3dtrue&type=meetup-join&deeplinkId=790029da-50aa-4d18-8864-45f9dc532ef1&directDl=true&msLaunch=true&enableMobilePage=true&suppressPrompt=true
org: PEDICINI Marco