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

  • 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)