<?xml version="1.0" encoding="ISO-8859-1" ?>
<rss version="2.0">
<channel>
<title>Marino Miculan's home site</title>
<link></link>
<description><![CDATA[Web page of Marino Miculan, associate professor of Computer Science at the University of Udine]]></description>
<item>
<title>Conferenza su Sicurezza delle reti (mobili) e Botnet</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=20</link>
<description><![CDATA[Come da tradizione, a conclusione del corso di Reti di Calcolatori e Sicurezza organizziamo un seminario tenuto da esperti aziendali su argomenti "caldi" di sicurezza delle reti.

Il tema di quest'anno è la sicurezza dei dispositivi mobili, in particolare l'avvento delle botnet su tali piattaforme.
A parlarne verranno il responsabile della Sicurezza informatica della Vodafone-Omnitel, Corradino Corradi, e due executive manager di Sicurezza della Accenture, Paolo Dal Cin e Paolo Colombo:]]></description>
</item>
<item>
<title>Esami di RCS e Reti</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=19</link>
<description><![CDATA[Come molti sapranno, con il passaggio dall'ordinamento ex DM 509/99 all'ordinamento ex DM 270/04, il corso di "Reti di Calcolatori e Sicurezza" è stato disattivato.]]></description>
</item>
<item>
<title>LFMTP 2010 post-proceedings</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=18</link>
<description><![CDATA[The post-proceedings of the 5th International Workshop on 
Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2010) have been published as volume 34 of EPTCS.]]></description>
</item>
<item>
<title>CTF RCS:2010: i risultati</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=17</link>
<description><![CDATA[Il contest RCS:2010 si è svolto il 23 giugno 2010.]]></description>
</item>
<item>
<title>CTF hacking contest RCS:2010</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=16</link>
<description><![CDATA[Quest'anno verrà organizzato un "Capture the flag" per gli studenti del corso di Reti di Calcolatori e Sicurezza.
In questo gioco, team di 2-4 studenti si sfidano ad una serie di challenge di sicurezza, che vanno dallo scoprire delle password a veri e propri attacchi (e difese) di hacking.]]></description>
</item>
<item>
<title>LFMTP site</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=13</link>
<description><![CDATA[The website of the 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice is online.
This year, LFMTP will be part of FLoC, affiliated with LICS 2010, and it will take place on July 14, in Edinburgh, Scotland.


Papers describing contributions on any theoretical or practical aspect of logical frameworks and metalanguages are welcome!]]></description>
</item>
<item>
<title>MeCBIC is online</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=15</link>
<description><![CDATA[The website of the 3rd Workshop on Membrane Computing and Biologically Inspired Process Calculi is online.
This workshop is affiliated with CONCUR 2009, and it will take place  on September 5, at the Bologna University, Italy.


Papers 
on the membrane systems or biologically inspired process calculi are sought.]]></description>
</item>
<item>
<title>ERASMUS 2009-2010</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=14</link>
<description><![CDATA[Il CRIN ha pubblicato il nuovo bando per la mobilità studentesca Erasmus/Socrates 2009-2010.]]></description>
</item>
<item>
<title>New publication (?)</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=12</link>
<description><![CDATA[Who says that nerds can do anything but coding and studying? Here is a counterexample: my picture of Murano has been published in the Schmap Venice Guide]]></description>
</item>
<item>
<title>PDFTKSIGN</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=11</link>
<description><![CDATA[Marco Del Toso has just submitted his BSc thesis: implementation of a command-line open-source tool for producing legally valid PDF files (using smartcards for signing).

Go to the Labs page for more details (and the relation, source code, etc.)]]></description>
</item>
<item>
<title>SAML in HLPSL</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=10</link>
<description><![CDATA[Riccardo Di Stasi has just submitted his Lab for the Computer Network Security course: formalization of Google Single-Sign-on protocol (based on SAML) in HLPSL and verification in AVISPA.
AVISPA finds the attack to the flawed version, and proves the safeness of the corrected (and now implemented) version of the protocol.


Go to the Labs page for more details (and the relation, source code, etc.)]]></description>
</item>
<item>
<title>Migration completed</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=9</link>
<description><![CDATA[Today I have completed the migration. Had to hack quite a bit the original SkyBlueCanvas code, but it is well worthwhile.]]></description>
</item>
<item>
<title>New Web Site</title>
<link>http:///~marino.miculan/index.php?pid=1&amp;show=8</link>
<description><![CDATA[As you may have noticed, the old site was too old and cumbersome.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=58</link>
<description><![CDATA[We present a non-invasive system for intrusion and anomaly detection, based on system call tracing in paravirtualized machines over Xen.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=57</link>
<description><![CDATA[We present a formal analysis of the authentication protocol of Facebook Connect, the Single Sign-On service offered by the Facebook Platform which allows Facebook users to login to affiliated sites.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=56</link>
<description><![CDATA[The Logical Frameworks and Meta-languages: Theory and Practice workshop aims to bring together designers, implementers, and practitioners working on these areas, and in particular about:


the automation and implementation of the meta-theory of programming languages and related calculi;
the design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology;
theoretical and practical issues concerning the encoding of variable bind]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=55</link>
<description><![CDATA[We give a stochastic extension of the Brane Calculus, along the lines of recent work by Cardelli and Mardare.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=54</link>
<description><![CDATA[Binding bigraphs are a graphical formalism intended to be a meta-model for mobile, concurrent and communicating systems.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=53</link>
<description><![CDATA[We introduce the Bio&#946; Framework, a meta-model for both protein-level and membrane-level interactions of living cells.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=52</link>
<description><![CDATA[We present a bigraphical framework suited for modeling biological systems both at protein level and 
at membrane level.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=51</link>
<description><![CDATA[We study the de&#64257;nition of a general abstract notion of barbed bisimilarity 
for reactive systems on bigraphs.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=50</link>
<description><![CDATA[We present DBtk, a toolkit for Directed Bigraphs.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=49</link>
<description><![CDATA[We give a formal connection between the graph grammars of Synchronized Hyperedge Replacement and 
Architectural Design Rewriting, and local bigraphs.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=2</link>
<description><![CDATA[We provide a categorical presentation of the Fusion calculus.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=21</link>
<description><![CDATA[These proceedings contain a selection of refereed papers presented at or related 
to the Annual Workshop of the TYPES project (EU coordination action 510996), 
which was held on May 2–5, 2007 in Cividale del Friuli (Udine), Italy.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=3</link>
<description><![CDATA[PiCNiC is a tool for verifying security properties of systems, namely non-interference properties of processes expressed as terms of the &#960;-calculus with two security levels and declassi&#64257;cation primitives.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=4</link>
<description><![CDATA[The aim of this work is to obtain an interactive proof environment based on Isabelle/HOL for reasoning formally about cryptographic protocols, expressed as processes of the spi calculus (a &#960;-calculus 
with cryptographic primitives).]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=5</link>
<description><![CDATA[We study the algebraic structure of directed bigraphs, a bigraphical model of computations with locations, 
connections and resources previously introduced as a unifying generalization of other variants of bigraphs.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=6</link>
<description><![CDATA[We study directed bigraph with negative ports, a bigraphical framework 
for representing models for distributed, concurrent and ubiquitous computing.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=7</link>
<description><![CDATA[The Brane Calculus is a calculus intended to model the structure and the dynamics of biological membranes.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=8</link>
<description><![CDATA[We study the construction of labelled transition systems 
from reactive systems de&#64257;ned over directed bigraphs, a computational 
meta-model which subsumes other variants of bigraphs.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=9</link>
<description><![CDATA[We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive 
Constructions, by taking advantage of Natural Deduction Semantics and coinduction in combination with weak Higher-Order Abstract Syntax and the Theory of Contexts.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=10</link>
<description><![CDATA[We introduce directed bigraphs, a bigraphical meta-model for describing computational paradigms dealing 
with locations and resource communications.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=11</link>
<description><![CDATA[We introduce directed bigraphs, a bigraphical meta-model for describing 
computational paradigms dealing with locations and resource communications.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=12</link>
<description><![CDATA[In this paper we survey some well-known approaches proposed as general models 
for calculi dealing with names (like for example process calculi with name-passing).]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=13</link>
<description><![CDATA[The Brane Calculus is a calculus of mobile processes, intended to model the transport machinery of a cell system.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=14</link>
<description><![CDATA[The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical 
account of the fundamental notions of variable and context as they appear in Higher 
Order Abstract Syntax.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=15</link>
<description><![CDATA[In questo articolo si descrive l’implementazione di una memoria 
distribuita condivisa (DSM) per un cluster di calcolatori connessi da 
un backplane CompactPCI, anziché da una normale rete a pacchetti.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=16</link>
<description><![CDATA[We study the relation between Nominal Logic and the Theory 
of Contexts, two approaches for specifying and reasoning about 
datatypes with binders.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=18</link>
<description><![CDATA[Abstract. We investigate a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular 
cases of the more general notion of distinction.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=17</link>
<description><![CDATA[We investigate a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular 
cases of the more general notion of distinction.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=24</link>
<description><![CDATA[In this paper, we model fresh names in the &#960;-calculus using abstractions with respect 
to a new binding operator &#952;.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=25</link>
<description><![CDATA[In this paper we present a theorem for de&#64257;ning &#64257;xed-points 
in categories of sheaves.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=26</link>
<description><![CDATA[This volume contains the Proceedings of the workshop COMETA 2003, held at the University of Udine (Italy), December 15–17,
2003.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=27</link>
<description><![CDATA[In recent years, many general presentations (meta models) for calculi with name-passing, either operational or denotational in &#64258;avour, have been proposed. In this 
paper, we investigate the connections among some of these proposals, namely permutation algebras, named sets and sheaf categories, with the aim of establishing a 
bridge between di&#64256;erent approaches to the abstract speci&#64257;cation of nominal calculi.

Get the PDF.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=29</link>
<description><![CDATA[In recent years, many general presentations (meta models) for calculi 
dealing with names, e.g.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=19</link>
<description><![CDATA[We investigate a framework for representing and reasoning 
about syntactic and semantic aspects of typed languages 
with variable binders.

First, we introduce typed binding signatures and develop 
a theory of typed abstract syntax with binders.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=20</link>
<description><![CDATA[We illustrate the bene&#64257;ts of using Natural Deduction in 
combination with weak Higher-Order Abstract Syntax for 
formalizing an ob ject-based calculus with ob jects, cloning, 
method-update, types with subtyping, and side-e&#64256;ects, in 
inductive type theories such as the Calculus of Inductive 
Constructions.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=22</link>
<description><![CDATA[We discuss the formalization of Abadi and Cardelli’s imp&#962; , a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type 
Theories, such as the Calculus of (Co)Inductive Constructions (CC(Co)Ind).]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=23</link>
<description><![CDATA[No description available.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=28</link>
<description><![CDATA[In this paper, we study the formalization of Abadi and Cardelli’s imp&#962;, a representative object-based calculus with types and side e&#64256;ects, in interactive proof assistants based on 
(Co)Inductive Type Theories, like Coq.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=30</link>
<description><![CDATA[In type theory based logical frameworks, recursive and corecursive de&#64257;nitions are subject to syntactic restrictions that ensure their 
termination and productivity.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=31</link>
<description><![CDATA[The Ambient Calculus has been recently proposed as a model of mobility of agents 
in a dynamically changing hierarchy of domains.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=48</link>
<description><![CDATA[No description available.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=32</link>
<description><![CDATA[Cheste vore e nas dilunc de preparazion dal dizionari dal Coretôr Ortografic Furlan 
(COF) de Societât Sientifiche e Tecnologjiche Furlane.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=33</link>
<description><![CDATA[We present two case studies in formal reasoning about untyped &#955;-calculus in Coq, 
using both &#64257;rst-order and higher-order abstract syntax.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=34</link>
<description><![CDATA[In recent years, logical frameworks and tile logic have been separately proposed by 
our research groups, respectively in Udine and in Pisa, as suitable metalanguages 
with higher-order features for encoding and studying nominal calculi. This paper 
discusses the main features of the two approaches, tracing di&#64256;erences and analogies 
on the basis of two case studies: late &#960;-calculus and lazy simply typed &#955;-calculus.

Get the PDF.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=35</link>
<description><![CDATA[We present a case study on the formal development of a non trivial (meta)theory in 
the Theory of Contexts using the Coq proof assistant.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=36</link>
<description><![CDATA[We present a logical framework &#933; for reasoning on a very 
general class of languages featuring binding operators, called nominal 
algebras, presented in higher-order abstract syntax (HOAS).]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=37</link>
<description><![CDATA[No description available.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=38</link>
<description><![CDATA[We present a Natural Deduction proof system for the propositional modal µ-calculus, and its formalization in the Calculus of Inductive Constructions.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=39</link>
<description><![CDATA[We present a large and we think also signi&#64257;cant case-study in computer 
assisted formal reasoning.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=40</link>
<description><![CDATA[No description available.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=41</link>
<description><![CDATA[We present a Natural Deduction proof system for the propositional modal µ-calculus, and its formalization in the Calculus of Inductive Constructions.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=42</link>
<description><![CDATA[In this paper, we present a formalization of Kozen’s propositional modal µ-calculus, 
in the Calculus of Inductive Constructions.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=43</link>
<description><![CDATA[We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=44</link>
<description><![CDATA[Nowadays, in many critical situations (such as on-board software), it is mandatory to certify programs and systems, that is, to prove formally that they meet their 
speci&#64257;cations.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=45</link>
<description><![CDATA[Natural Deduction style presentations of program logics are 
useful in view of the implementation of such logics in interactive proof 
development environments, based on type theory, such as LEGO, Coq, 
etc.]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=46</link>
<description><![CDATA[We introduce a new paradigm for concurrency, called 
"behaviours-as-types".]]></description>
</item>
<item>
<title></title>
<link>http:///~marino.miculan/index.php?pid=9&amp;show=47</link>
<description><![CDATA[We explore the expressive power of the formalism called Natural Operational Semantics, NOS, introduced by Burstall and Honsell for 
de&#64257;ning the operational semantics of programming languages.]]></description>
</item>
<item>
<title>Marino Miculan</title>
<link>http:///~marino.miculan/index.php?pid=1</link>
<description><![CDATA[Marino Miculan, PhD

Associate Professor of Computer Science (INF/01) at the Faculty of Science of the University of Udine.&nbsp;

Address: Department of Mathematics and Computer Science (DiMI), Università di Udinevia delle Scienze 208, I-33100 Udine (Italy).
Office location: L2.17.BC, also known as SN6.]]></description>
</item>
<item>
<title>About Marino Miculan</title>
<link>http:///~marino.miculan/index.php?pid=7</link>
<description><![CDATA[Bio sketch
I got my PhD in Computer Science at the University of Pisa in 1997.
From 1997 to 2000 I have been research engineer at the INFN, Trieste.]]></description>
</item>
<item>
<title>Marino Miculan's latest news</title>
<link>http:///~marino.miculan/index.php?pid=5</link>
<description><![CDATA[]]></description>
</item>
<item>
<title>Marino Miculan's publications</title>
<link>http:///~marino.miculan/index.php?pid=9</link>
<description><![CDATA[]]></description>
</item>
<item>
<title>Marino Miculan's teaching activity</title>
<link>http:///~marino.miculan/index.php?pid=8</link>
<description><![CDATA[Corsi dell'A.A.]]></description>
</item>
<item>
<title>Marino Miculan: argomenti per Laboratori Avanzati e Tesi di Laurea</title>
<link>http:///~marino.miculan/index.php?pid=10</link>
<description><![CDATA[Laboratori avanzati e Tesi di laurea

Qui descrivo alcuni argomenti generali di mio interesse, su cui
è possibile svolgere dei laboratori avanzati o tesi di laurea (triennale o specialistica).
Se qualche argomento è di vostro interesse, possiamo fissare un
appuntamento per discutere un progetto preciso (la cui disponibilità
varia nel tempo).


Regole generali:

 I progetti vengono assegnati su base "first-come
first-served, con time-out": quando un progetto viene assegnato, si
fissa]]></description>
</item>
<item>
<title>Photos from Marino Miculan</title>
<link>http:///~marino.miculan/index.php?pid=12</link>
<description><![CDATA[Photography

Maybe I spend too much time on photography, but it is so much fun…  I have some web photo albums on Google Picasa, on NGM MyShots, on Panoramio.]]></description>
</item>
<item>
<title>Other from Marino Miculan</title>
<link>http:///~marino.miculan/index.php?pid=11</link>
<description><![CDATA[Open source
 I advocate the use of open source software (although I still use Mac OS X, as it is the best OS around at the moment).]]></description>
</item>
<item>
<title>Test page</title>
<link>http:///~marino.miculan/index.php?pid=4</link>
<description><![CDATA[questa pagina è quasi vuota]]></description>
</item>
<item>
<title>Marino Miculan: Reti di Calcolatori e Sicurezza</title>
<link>http:///~marino.miculan/index.php?pid=13</link>
<description><![CDATA[Corso di Reti di Calcolatori e Sicurezza – A.A.]]></description>
</item>
</channel>
</rss>
