Caros Colegas, Depois da visita da Carolyn Talcott do SRI, eu estou recebendo pelos próximos dias a visita do Prof. Martin Hofmann, até o dia 14/06, aqui em João Pessoa. Talvez interessem a comunidade de lógica o tema que ele estará falando no nosso seminário da pós-graduação em informática (SPIN). O título e abstract da apresentação seguem abaixo.
A apresentação será na escola de redes da UFPB nesta sexta-feira (07/06) das 10 - 12h. Abraços, Vivek Título: Proof-Relevant Logical Relations Abstract: We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves two well-known problems caused by the use of existential quantification over future worlds in traditional Kripke logical relations: failure of admissibility, and spurious functional dependencies. We illustrate the novel format with two applications: a direct-style validation of Pitts and Stark's equivalences for ``new'' and a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked; non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module soundly to validate more effect-based program equivalences than would be possible with traditional effect systems. _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
