@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"}

  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
		  \item[1] Preliminaries
	     	  \item[2] Syntax
	     	  \item[3] Labelled semantics
	     	    \item[3.1] Late semantics
	     	    \item[3.2] Early semantics
	     	    \item[3.3] Open semantics
  linkhtmlabs =	 "",
  linkdvi =	 "",
  linkps =	 "",
  linkpdf =	 ""

  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 " #
  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
	     	  \item[1] Background and introduction
	     	    \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
	     	  \item[2] Normalization by evaluation
	     	    \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
	     	  \item[3] Offline type-directed partial evaluation
	     	    \item[3.1] The power function, part 1
	     	    \item[3.2] The power function, part 2
	     	    \item[3.3] Summary and conclusion
	     	  \item[4] Online type-directed partial evaluation
	     	    \item[4.1] Online simplification for integers
	     	    \item[4.2] The power function, revisited
	     	    \item[4.3] Summary and conclusion
	     	  \item[5] Incremental type-directed partial evaluation
	     	  \item[6] Conclusion and issues
  linkhtmlabs =	 "",
  OPTlinkdvi = 	 "",
  OPTlinkps = 	 "",
  OPTlinkpdf = 	 ""

  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.
	     	  \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
  linkhtmlabs =	 "",
  linkdvi =	 "",
  linkps =	 "",
  linkpdf =	 ""

  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
	       	    \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
	       	    \item[6] Negative translation and its use combined with
		             functional interpretation
	       	    \item[7] The Friedman A-translation
	       	    \item[8] Final comments
  linkhtmlabs =	 "",
  linkdvi =	 "",
  linkps =	 "",
  linkpdf =	 ""