Papers by Pietro Di Gianantonio

Real Number Computability

A language for differentiable function (extended version).
Pietro Di Gianantoni, Abbas Edalat
Proc. of the conference FOSSACS '13; LNCS. [pdf copy]
A certified, corecursive implementation of exact real numbers.
Alberto Ciaffaglione, Pietro Di Gianantonio.
Theoretical Computer Science, 2006, vol. 351, pp. 39-51. [pdf copy]
A tour with constructive real numbers.
Alberto Ciaffaglione, Pietro Di Gianantonio.
[pdf copy]
A co-inductive approach to real numbers.
Alberto Ciaffaglione, Pietro Di Gianantonio.
Proc. of the workshop Types for Proofs and Programs - Types '99; LNCS 1956, pp. 114-130. [pdf copy]
An abstract data type for real numbers.
Pietro Di Gianantonio.
Theoretical Computer Science, 1999, vol. 221, n. 1-2, pp. 295-326; [pdf copy]
extended version of a paper presented at ICALP '97, LNCS 1256, pp. 121-131. [pdf copy]
A golden notation for real numbers.
Pietro Di Gianantonio.
CWI technical report. [pdf copy]
Real number computability and domain theory.
Pietro Di Gianantonio.
Information and Computation, 1996, vol. 127, n. 1, pp. 12-25,
extended version of a paper presented at MFCS '93. [pdf copy]
A functional approach to computability on real numbers.
Pietro Di Gianantonio.
Ph.D. Thesis: Universita di Pisa-Genova-Udine. [pdf copy]

Process Calculi

Efficient bisimilarities from second-order reaction semantics for pi-calculus.
Pietro Di Gianantonio, Svetlana Jaksic, Marina Lenisa.
Proc. of Concur'10 -; LNCS 6269, pp. 358-372. [pdf copy]
Extended version: [pdf copy]
Finitely branching LTS's from reaction semantics for process calculi
Pietro Di Gianantonio, Furio Honsell, Marina Lenisa.
Proc. of the Workshop on Algebraic Development Techniques - WADT'08; LNCS 5484, pp. 119-134. [pdf copy]

Lambda Calculus and Game Semantics

An implementation of an algorithm for constructing principal types of lambda terms.
[An Haskell program.]
Innocent game semantics via intersection type assignment systems
Pietro Di Gianantonio, Marina Lenisa.
Proc. of the conference CSL '13; LIPIcs 4962, pp. 334-349. [pdf copy] [slides]
RPO, second-order contexts, and lambda-calculus
Pietro Di Gianantonio, Furio Honsell, Marina Lenisa.
Proc. of the conference FOSSACS '08; LNCS 4962, pp. 334-349. [pdf copy] Extended version appeared on Logical Methods in Computer Science, 2009, vol. 5, n. 2: [pdf copy]
Oracle game semantics for the nu-calculus
Pietro Di Gianantonio, Marino Miculan.
Submitted for pubblication. [pdf copy]
A type assignment system for game semantics
Pietro Di Gianantonio, Furio Honsell, Marina Lenisa.
Theoretical Computer Science , 2008, vol. 398, pp. 150-169. [pdf copy]
Games characterizing Levy-Longo trees.
Luke Onk, Pietro Di Gianantonio.
Theoretical Computer Science , 2004, vol. 312, pp. 121-142. [pdf copy]
Extended version of a paper presented at Int. Colloquium on Automata Language and Programming (ICALP '02); LNCS 2380, pp. 476-487. [pdf copy]
Game semantics for the pure lazy lambda-calculus.
Pietro Di Gianantonio.
Proc. of the conference Typed Lambda Calculus and Applications (TLCA '01); LNCS 2044, pp 106-120. [pdf copy]
The fine structure of game lambda-models.
Pietro Di Gianantonio, Gianluca Franco.
Extended version of a paper presented at Foundation of Software Technology and Theoretical Computer Science (FSTTS '00); LNCS 1974, pp. 429-441. [pdf copy]
A type assignment system for the game semantics.
Pietro Di Gianantonio, Gianluca Franco.
Proc. of Italian Conference on Theoretical Computer Science '98; World Scientific, pp. 37-47. [pdf copy]
Game semantic for untyped lambda calculus.
Pietro Di Gianantonio, Gianluca Franco, and Furio Honsell.
Proc. of the conference Typed Lambda Calculus and Applications '99; LNCS 1591, pp 114-128. [pdf copy]
A lambda calculus of objects with self-inflicted extension.
Pietro Di Gianantonio, Furio Honsell and Luigi Liquori.
Proc. of OOPSLA '98, International Symposium on Object Oriented, Programming, System, Languages and Applications; ACM PRESS, 1998, pp. 166-178. [pdf copy]
Uncountable Limits and the Lambda Calculus.
Pietro Di Gianantonio, Furio Honsell and Gordon D. Plotkin.
Nordic Journal of Computing, 1995, vol. 2, n. 2, pp 126-145,
extended version of a paper presented at CONCUR-94. [pdf copy]
An abstract notion of application.
Pietro Di Gianantonio and Furio Honsell.
Proc. of the conference Typed Lambda Calculus and Applications 93; LNCS 664, pp 124-138. [pdf copy]

Proof Theory

Structures in cyclic linear logic.
Pietro Di Gianantonio.
Computer Science Logic (CLS '04); LNCS 3210, pp. 130-144. [pdf copy]
Unifying recursive and co-recursive definitions in sheaf categories.
Pietro Di Gianantonio, Marino Miculan.
Int. Converence on Foundations of Software Science and Computation Structures (FOSSACS '04); LNCS 2897, pp. 136-150. [pdf copy]
A unifying approach to recursive and co-recursive definitions.
Pietro Di Gianantonio, Marino Miculan.
Workshop on Types for Proofs and Programs (Types '02); LNCS 2003, pp. 148-161. [pdf copy]