 IDEALS Home
 →
 Browse by Author
Browse by Author "Popescu, Andrei"
Now showing items 115 of 15

Popescu, Andrei; Rosu, Grigore (200505)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
PDF (332Kb) 
Popescu, Andrei (20110114)We develop a theory of syntax with bindings, focusing on:  methodological issues concerning the convenient representation of syntax;  techniques for recursive definitions and inductive reasoning. Our approach ...
application/pdf
PDF (1Mb) 
Popescu, Andrei (200903)Combining traces, coalgebra and lazyfiltering channel configurations for parallel composition, we give a fullyabstract denotational semantics for the picalculus under weak early bisimilarity.
application/pdf
PDF (627Kb) 
Popescu, Andrei (200903)Combining traces, coalgebra and lazyfiltering channel configurations for parallel composition, we give a fullyabstract denotational semantics for the picalculus under weak early bisimilarity.
application/pdf
PDF (627Kb) 
Popescu, Andrei; Rosu, Grigore (200607)Generic firstorder logic (GFOL) is a firstorder logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution ...
application/pdf
PDF (567Kb) 
Popescu, Andrei (20090511)We develop some HigherOrder 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 hasslefree ...
application/pdf
PDF (380Kb) 
Popescu, Andrei (2010)This collection of documents presents the Isabelle formalization of HigherOrder Abstract Syntax (HOAS) as a definitional layer on top of FirstOrder Abstract Syntax (FOAS). The formal scripts shown here are provided as a ...
application/zip
ZIP (3Mb) 
Popescu, Andrei; Gunter, Elsa L. (20100128)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
PDF (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
ZIP (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 lambdacalculus.
application/zip
ZIP (2Mb) 
Popescu, Andrei (20100128)
application/zip
ZIP (772Kb) 
Popescu, Andrei; Serbanuta, Traian Florin; Rosu, Grigore (200505)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 firstorder ...
application/pdf
PDF (309Kb) 
Popescu, Andrei; Gunter, Elsa L.; Osborn, Christopher J. (2010)We present a point of view concerning HOAS (HigherOrder 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
PDF (182Kb) 
Popescu, Andrei; Rosu, Grigore (200901)Termgeneric logic (TGL) is a firstorder 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
PDF (666Kb) 
Popescu, Andrei; Rosu, Grigore (200901)Termgeneric logic (TGL) is a firstorder 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
PDF (666Kb)
Now showing items 115 of 15