AMADIO's publications

---

IMPORTANT You can retrieve documents in postscript gzipped format. If you click on the title, you should get some non-sense (the gzipped code). Save the non-sense in a file (using the --save as-- command of your browser), say foo.gz, and then gunzip it to get the postscript. Please note that ftp is not supported.

---

BOOK: Domains and Lambda Calculi
by Roberto Amadio and Pierre-Louis Curien, published by Cambridge University Press.
Here are the official reference at CUP web site, the reference for the US, and the Preface and Index in postscript and plain text.
A review of the book by F. Cardone has appeared in Science of Computer Programming, nr 35, 1999. Another review by D.L. Chester, is appeared in Computing Reviews, October 1999, page 460. Yet another review appeared in Zentralblatt Math. 962 (2001) by P. Severi.
Mistakes in the book we are aware of.


---

Some bibliographic references as tracked by DBLP. Many pre-prints are available in HAL and some of them are mirrored in ArXiV. Searching publications containing Amadio among the authors will do.


---

SOME PRE-PRINTS (electronic version available)

---

• Certifying and reasoning on cost annotations of functional programs.
  R.M. Amadio, Y. Régis-Gianas.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, October 2011. Extended abstract in Proc. FOPARA 2011, Springer LNCS.

• Elementary affine lambda-calculus with multithreading and side effects.
  A. Madet, R.M. Amadio.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, February 2011. Extended abstract in Typed Lambda Calculi and Applications 2011, Springer LNCS.

• A decompilation of the pi-calculus and its application to termination.
  R.M. Amadio.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, February 2011.

• Certifying cost annotations in compilers.
  R.M. Amadio, N. Ayache, Y. Régis-Gianas, and R. Saillard.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, October 2010.

• An affine-intuitionistic system of types and effects: confluence and termination.
  R.M. Amadio, P. Baillot, and A. Madet.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, December 2009. Presented at LOLA 2010 Workshop on Syntax and semantics of low level languages.

• On stratified regions.
  R.M. Amadio.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, April 2009.
  Short version in Proc. APLAS 2009, Springer LNCS.
  A presentation of this work.

• On convergence sensitive bisimulation and the embedding of CCS in timed CCS.
  R.M. Amadio.
  Technical Report, Université Diderot (Paris 7), Laboratoire PPS, June 2008. Revised version in Express 08, appeared in Electronic Notes in TCS 242, 2009. A presentation of this work given at Express 08.
  

• On affine usages in signal-based communication.
  R.M. Amadio and M. Dogguy.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, April 2008. Revised version in APLAS 08 (to appear in Springer LNCS).
  

• Determinacy in a synchronous pi-calculus.
  R.M. Amadio and M. Dogguy.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, July 2007.
  Revised version to appear in the book `From semantics to computer science: essays in honor of Gilles Kahn', Cambridge University Press.
  

• Feasible reactivity in a synchronous pi-calculus.
  R.M. Amadio and F. Dabrowski.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, February 2007.
  Revised short version in Proc. ACM SIGPLAN Symp. on Principles and Practice of Declarative Programming, 2007. A presentation of this work given at PPDP 2007.
  

• A synchronous pi-calculus.
  R.M. Amadio.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, June 2006.
  A presentation of this work given at Emerging Trends in Concurrency Theory (LIX, Palaiseau). A revised version of this paper appears in Information and Computation, 205(9):1470--1490, 2007.

• The SL synchronous language, revisited.
  R.M. Amadio.
  Technical Report, Université Paris Diderot (Paris 7), Laboratoire PPS, November 2005. Revised version appeared in Journal of Logic and Algebraic Programming, 70, pp 121-150, 2007.

• Feasible reactivity for synchronous cooperative threads.
  R.M. Amadio, F. Dabrowski.
  Extended abstract presented at the workshop Expressiveness in Concurrency, San Francisco, September 2005. Revised version in Electronic Notes in TCS 154, Issue 3, 2006.

• Reactive concurrent programming revisited.
  R.M. Amadio, G. Boudol, F. Boussinot, I. Castellani.
  Extended abstract presented at the workshop Algebraic Process Calculi: the first twenty five years and beyond, Bertinoro, August 2005. Revised version in Electronic Notes in TCS, 162:49-90, 2006.

• Resource control for synchronous cooperative threads.
  R.M. Amadio, S. Dal Zilio.
  Research Report LIF, May 2004. Extended abstract in Proc. CONCUR 2004, Springer LNCS. Revised version in Theoretical Computer Science 358:229--254, 2006..

• A functional scenario for bytecode verification of resource bounds.
  R.M. Amadio, S. Coupet-Grimal, S. Dal Zilio, L. Jakubiec.
  Research Report LIF 17-2004, January 2004. Extended abstract in Proc. CSL 2004, Springer LNCS. Short version presented at SPACE 2004 (Semantics, program analysis, and computing environments for memory management).

• Synthesis of max-plus quasi-interpretations.
  R.M. Amadio.
  Research Report LIF 18-2004, January 2004.
  Fundamenta Informaticae, 65(1--2):29-60, 2005.

• Max-plus quasi-interpretations.
  R.M. Amadio.
  Research Report LIF 10-2002, December 2002. Extended abstract in Typed Lambda Calculi and Applications (TLCA) 2003. Springer-Lecture Notes in Computer Science.

• On name generation and set-based analysis in Dolev-Yao model.
  R.M. Amadio and W. Charatonik.
  INRIA Research Report 4379, January 2002. Extended abstract in Proc. CONCUR 02, Springer-Lecture Notes in Computer Science 2421.

• On decidability of the control reachability problem in the asynchronous pi-calculus.
  R.M. Amadio and Ch. Meyssonnier.
  Nordic Journal of Computing, volume 9, number 2, pages 70-101, 2002, Pre-print available as RR LIF 04-2002 at this address. Preliminary version appeared in Electronic Notes in Theoretical Computer Science, Proceedings EXPRESS 2001, Aalborg and as INRIA Research Report 4241, August 2001 with the title `On the decidability of fragments of the asynchronous pi-calculus'.

• On the symbolic reduction of processes with cryptographic functions
  R.M. Amadio, D. Lugiez, V. Vanackere
  Theoretical Computer Science, 290(1):695--740, 2002.
  Also INRIA Research Report 4147, March 2001.

• On the reachability problem in cryptographic protocols
  R.M. Amadio, D. Lugiez
  INRIA Research Report 3915, March 2000. Extended abstract appeared in Springer LNCS 1877 as Proc. of CONCUR 00, State College. A generalization to public keys and an implementation of this work in collaboration with Vincent Vanackere has been presented at the Workshop on Issues in the theory of security (Wits 00), Geneve, July 2000.

• The game of the name in cryptographic tables
  R.M. Amadio, S. Prasad
  INRIA Research Report 3733, July 1999. Extended abstract in the Springer LNCS 1742 as Proc. of ASIAN 99, Phuket, Thailand.

• The receptive distributed pi-calculus
  R.M. Amadio, G. Boudol, C. Lhoussaine
  Presented at 5th Mobile Objects Systems Workshop, Lisbon, June 1999. Extended abstract in the Springer LNCS 1738 as Proc of FST-TCS99, Madras.
  A longer version appeared as INRIA Research Report 4080. Two revised reports are now available as RR LIF 05-2002 (also appeared in Fundamenta Informaticae, 53(2):105--129, 2002) and RR LIF 06-2002 (also appeared in ACM-TOPLAS, Vol 25, No 5, September 2003, Pages 1-29).

• On modelling mobility
  R.M. Amadio
  Journal of Theoretical Computer Science, 240 : 147-176, 2000.

• Analysis of a guard condition in type theory (Preliminary report)
  R.M. Amadio S. Coupet-Grimal
  Rapport Interne 245, Laboratoire d'Informatique de Marseille October 1997 and Rapport de Recherche INRIA 3300. Extended abstract ETAPS 98 (FoSSaCS), SLNCS 1378.

• Modelling IP Mobility
  R.M. Amadio S. Prasad
  Rapport Interne 244, Laboratoire d'Informatique de Marseille October 1997 and and Rapport de Recherche INRIA 3301. Promela sources for FMob Extended abstract appeared in Proc. of CONCUR 98 (Nice), SLNCS 1466. Revised and extended version in Journal of Fomal Methods in Systems Design, 17(1) :61--99, 2000.

• An asynchronous model of locality, failure, and process mobility
  R.M. Amadio
  In COORDINATION 97, SLNCS 1282, Berlin, 1997.
  Also Rapport Interne 216 LIM February 1997, and INRIA Research Report 3109.

• On bisimulations for the asynchronous pi-calculus
  Amadio R., I. Castellani, and D. Sangiorgi
  In CONCUR 96, SLNCS 1119, Pisa, 1996 (Revised and extended version in a special issue of TCS)

• Toward a modal theory of types for the pi-calculus
  R. Amadio and M. Dam
  In Proc. Formal Techniques in Real Time and Fault Tolerant Systems 96, Uppsala. SLNCS 1135, 1996

• From a concurrent lambda-calculus to the pi-calculus
  R. Amadio, L. Leth, and B. Thomsen
  In Proc. Foundations of Computation Theory 95, Dresden. SLNCS 965, 1995

• Reasoning about higher-order processes
  R. Amadio and M. Dam
  In Proc. CAAP 95, Aarhus. SLNCS 915, 1995

• Localities and Failures
  R.M. Amadio and S. Prasad
  In P~S Thiagarajan, editor , Proceedings of $14^th$ FST and TCS Conference, FST-TCS'94, volume 880 of SLNCS, pages 205--216. Springer-Verlag, 1994

• Translating core facile
  R. Amadio
  Technical Report ECRC-94-3, ECRC, Munich, 1994

• An analysis of pi-calculus bisimulations
  R. Amadio and O. Ait-Mohamed
  Technical Report 94-2, European Computer-Industry Research Center, Munich, 1994

• On the reduction of Chocs bisimulation to pi-calculus bisimulation
  R. Amadio
  In Proc. CONCUR 93, Hildesheim, pages 112--126. SLNCS 715, 1993

  ---

  SOME OLDER REFERENCES (pre-prints of some of them are available in HAL)

  ---

• Type equations in the models of languages with parametric types (equazioni tra tipi nei modelli di linguaggi con tipi parametrici)
  R. Amadio
  Master's thesis, Università di Pisa, 1985.

• The finitary projection model and the solution of higher order domain equations
  R. Amadio, K. Bruce, and G. Longo
  In Proc. IEEE Conference on Logic in Computer Science (LICS), Boston, pages 122--130. IEEE, 1986.

• Type-free compiling of parametric types
  R. Amadio and G. Longo
  In M. Wirsing, editor , Formal Description of Programming Concepts-III, pages 377--398. IFIP, North Holland, 1987.

• Languages and models
  R. Amadio and G. Longo
  Technical report, Carnegie Mellon University, Pittsburgh, 1988.

• A fixed point extension of the second order lambda calculus: observational equivalences and models
  R. Amadio
  In Proc. IEEE Conference on Logic in Computer Science (LICS), Edinburgh, pages 51--60. IEEE, 1988.

• Formal theories of inheritance for typed functional languages
  R. Amadio
  Technical report, Dipartimento di Informatica, Università di Pisa, 1989.

• Recursion and Subtyping in Lambda Calculi
  R. Amadio
  PhD thesis, Università di Pisa, 1990.

• Typed equivalence, type assignment and type containment
  R. Amadio
  In Kaplan and Okada, editors , Proc. Conditional and Typed Rewriting Systems 90, pages 372--382. SLNCS 516, 1990.

• Bifinite domains: Stable case
  R Amadio
  In Pitt &al., editor , Proc. Category Theory in Comp. Sci. 91, Paris, pages 16--33. SLNCS 530, 1991.

• Domains in a realizability framework
  R. Amadio
  In Abramsky and Maibaum, editors , Proc. CAAP 91, Brighton, pages 241--263. SLNCS 493, 1991.

• Recursion over realizability structures
  R. Amadio
  Information and Computation, 91(1):55--85, 1991.

• A uniform presentation of chocs and pi-calculus
  R. Amadio
  Research Report 1726, Inria-Lorraine, 1992.

• On the adequacy of per models
  R. Amadio
  In Proc. Mathematical Foundations of Computer Science, Gda'nsk, Poland, pages 222--231. SLNCS 711, 1993.

• Subtyping recursive types
  R. Amadio and L. Cardelli
  ACM-TOPLAS, 15(4):575--631, 1993. Preliminary version in POPL 91.

• Trois Lambda-Calculs
  R. Amadio
  Habilitation, Universitè Nancy 1, Henri Poincaré, 1994.

• Selected domains and lambda calculi
  R. Amadio and P.-L. Curien
  Technical Report 161, INRIA-Lorraine, 1994. Preliminary version of the book Domains and Lambda-calculi

• A quick construction of a retraction of all retractions for stable bifinites
  R. Amadio
  Information and Computation, 116(2):272--274, 1995.