Browse Research and Tech Reports - Computer Science by Author "Popescu, Andrei"

  • Popescu, Andrei; Rosu, Grigore (2005-05)
    We show that any institution I satisfying some reasonable conditions can be transformed into another institution, Ib, which captures formally and abstractly the intuitions of adding support for behavioral equivalence and ...

    application/pdf

    application/pdfPDF (332Kb)
  • Popescu, Andrei (2009-03)
    Combining traces, coalgebra and lazy-filtering channel configurations for parallel composition, we give a fully-abstract denotational semantics for the pi-calculus under weak early bisimilarity.

    application/pdf

    application/pdfPDF (627Kb)
  • Popescu, Andrei (2009-03)
    Combining traces, coalgebra and lazy-filtering channel configurations for parallel composition, we give a fully-abstract denotational semantics for the pi-calculus under weak early bisimilarity.

    application/pdf

    application/pdfPDF (627Kb)
  • Popescu, Andrei; Rosu, Grigore (2006-07)
    Generic first-order logic (GFOL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution ...

    application/pdf

    application/pdfPDF (567Kb)
  • Popescu, Andrei (2009-05-11)
    We develop some Higher-Order Abstract Syntax (HOAS) concepts and proof principles as a collection of definitions and propositions on top of the original syntax with bindings. Our approach brings together hassle-free ...

    application/pdf

    application/pdfPDF (380Kb)
  • Popescu, Andrei; Gunter, Elsa L. (2010-01-28)
    We present a coinductive proof system for bisimilarity in transition systems specifiable in the de Simone SOS format. Our coinduction is incremental, in that it allows building incrementally an a priori unknown bisimulation, ...

    application/pdf

    application/pdfPDF (325Kb)
  • Popescu, Andrei (2010)
    This is a browsable html document presenting an Isabelle formalization of a general theory of syntax with static bindings and substitution.

    application/zip

    application/zipZIP (3Mb)
  • Popescu, Andrei (2010)
    This document presents and Isabelle formalization of a general theory of syntax with bindings. It also includes some case studies from the theory of lambda-calculus.

    application/zip

    application/zipZIP (2Mb)
  • application/zip

    application/zipZIP (772Kb)
  • Popescu, Andrei; Serbanuta, Traian Florin; Rosu, Grigore (2005-05)
    Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify more than twenty interpolation results for first-order ...

    application/pdf

    application/pdfPDF (309Kb)
  • Popescu, Andrei; Gunter, Elsa L.; Osborn, Christopher J. (2010)
    We present a point of view concerning HOAS (Higher-Order Abstract Syntax) and an extensive exercise in HOAS along this point of view. The point of view is that HOAS can be soundly and fruitfully regarded as a {\em ...

    application/pdf

    application/pdfPDF (182Kb)
  • Popescu, Andrei; Rosu, Grigore (2009-01)
    Term-generic logic (TGL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying ...

    application/pdf

    application/pdfPDF (666Kb)
  • Popescu, Andrei; Rosu, Grigore (2009-01)
    Term-generic logic (TGL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying ...

    application/pdf

    application/pdfPDF (666Kb)