@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@TechReport{BRICS-LS-98-4,
author = "Quaglia, Paola",
title = "The $\pi$-Calculus: Notes on Labelled Semantics",
institution = brics,
year = 1998,
type = ls,
number = "LS-98-4",
address = daimi,
month = dec,
note = "viii+16~pp",
abstract = "The $\pi$-calculus is a name-passing calculus that allows
the description of distributed systems with a dynamically
changing interconnection topology. Name communication,
together with the possibility of declaring and exporting
local names, gives the calculus a great expressive power.
For instance, it was remarkably shown that
process-passing calculi, that express mobility at higher
order, can be naturally encoded in $\pi$-calculus.\bibpar
Since its very first definition, the $\pi$-calculus
proliferated in a family of calculi slightly departing
the one another either in the communication paradigm
(polyadic vs monadic, asynchronous vs synchronous) or in
the bisimulation semantics (labelled vs unlabelled, late
vs early vs open vs barbed vs \ldots).\bibpar
These short notes present a collection of the labelled
strong semantics of the (synchronous monadic)
$\pi$-calculus. The notes could not possibly substitute
any of the standard references listed in the
Bibliography. They rather represent an attempt to group
together, using a uniform notation and the terminology
that got assessed over the last years, a few definitions
and concepts otherwise scattered throughout the
$\pi$-calculus literature.yy
\subsubsection*{Contents}
\begin{itemize}
\item[1] Preliminaries
\item[2] Syntax
\item[3] Labelled semantics
\begin{itemize}
\item[3.1] Late semantics
\item[3.2] Early semantics
\item[3.3] Open semantics
\end{itemize}
\end{itemize}",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@TechReport{BRICS-LS-98-3,
author = "Danvy, Olivier",
title = "Type-Directed Partial Evaluation",
institution = brics,
year = 1998,
type = ls,
number = "LS-98-3",
address = daimi,
month = dec,
note = "Extended version of lecture notes to appear in " #
lncspept98,
abstract = "Type-directed partial evaluation uses a normalization
function to achieve partial evaluation. These lecture
notes review its background, foundations, practice, and
applications. Of specific interest is the modular
technique of offline and online type-directed partial
evaluation in Standard ML of New Jersey
\subsubsection*{Contents}
\begin{itemize}
\item[1] Background and introduction
\begin{itemize}
\item[1.1] Partial evaluation by normalization
\item[1.2] Prerequisites and notation
\item[1.3] Two-level programming in ML
\item[1.4] Binding-time coercions
\item[1.5] Summary and conclusion
\end{itemize}
\item[2] Normalization by evaluation
\begin{itemize}
\item[2.1] A normalization function
\item[2.2] Application to decompilation
\item[2.3] Normalization by evaluation
\item[2.4] Naive normalization by evaluation in ML
\item[2.5] Towards type-directed partial evaluation
\item[2.6] Normalization by evaluation in ML
\item[2.7] Summary and conclusion
\end{itemize}
\item[3] Offline type-directed partial evaluation
\begin{itemize}
\item[3.1] The power function, part 1
\item[3.2] The power function, part 2
\item[3.3] Summary and conclusion
\end{itemize}
\item[4] Online type-directed partial evaluation
\begin{itemize}
\item[4.1] Online simplification for integers
\item[4.2] The power function, revisited
\item[4.3] Summary and conclusion
\end{itemize}
\item[5] Incremental type-directed partial evaluation
\item[6] Conclusion and issues
\end{itemize}",
linkhtmlabs = "",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = ""
}
@TechReport{BRICS-LS-98-2,
author = "Carsten Butz",
title = "Regular Categories and Regular Logic",
institution = brics,
year = 1998,
type = ls,
number = "LS-98-2",
address = daimi,
month = oct,
OPTnote = "viii+35~pp",
abstract = "Notes handed out to students attending the course on
Category Theory at the Department of Computer Science in
Aarhus, Spring~1998. These notes were supposed to give
more detailed information about the relationship between
regular categories and regular logic than is contained in
Jaap van Oosten's script on category theory (BRICS
Lectures Series LS-95-1). Regular logic is there called
coherent logic.
\subsubsection*{Contents}
\begin{itemize}
\item[1] Prologue
\item[2] Regular Categories
\item[3] Regular Logic
\item[4] A Sound Calculus
\item[5] The Internal Logic of a Regular Category
\item[6] The Generic Model of a Regular Theory
\item[7] Epilogue
\end{itemize}",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@TechReport{BRICS-LS-98-1,
author = "Kohlenbach, Ulrich",
title = "Proof Interpretations",
institution = brics,
year = 1998,
type = ls,
number = "LS-98-1",
address = daimi,
month = jun,
OPTnote = "viii+70~pp",
abstract = "These lecture notes are a polished version of notes from
a BRICS PhD course given in the spring term 1998.\bibpar
Their purpose is to give an introduction to two major
proof theoretic techniques: functional interpretation and
(modified) realizability. We focus on the possible use
of these methods to extract programs, bounds and other
effective data from given proofs.\bibpar
Both methods are developed in the framework of
intuitionistic arithmetic in higher types.\bibpar
We also discuss applications to systems based on
classical logic. We show that the combination of
functional interpretation with the so-called negative
translation, which allows to embed various classical
theories into their intuitionistic counterparts, can be
used to unwind non-constructive proofs.\bibpar
Instead of combining functional interpretation with
negative translation one can also use in some
circumstances a combination of modified realizability
with negative translation if one inserts the so-called
A-translation (due to H. Friedman) as an intermediate
step.
\subsubsection*{Contents}
\begin{itemize}
\item[1] Introduction: Unwinding proofs
\item[2] Intuitionistic logic and arithmetic in all
finite types
\item[3] Modified realizability
\item[4] Majorizability and the fan rule
\item[5] G{\"o}del's functional
(`Dialectica-')interpretation
\item[6] Negative translation and its use combined with
functional interpretation
\item[7] The Friedman A-translation
\item[8] Final comments
\end{itemize}",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}