Journal publications

F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell, M. Lenisa, I. Scagnetto
LF+ in Coq for "fast and loose" reasoning, Journal of Formalized Reasoning, 12(1), 2020, 11--51.
Available at: https://jfr.unibo.it/article/view/9757


F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic, I. Scagnetto
An Open Logical Framework, Journal Logic Computation, 26(1), 2016, 293--335, DOI 10.1093/logcom/ext028.
[Abstract] [ pdf-copy]

M. Lenisa
Multigames and strategies, coalgebraically, Theoretical Computer Science, 604, 2015, 46--62, DOI 10.1016/j.tcs.2015.07.020.
[Abstract] [ pdf-copy]

F. Honsell, M. Lenisa, D. Pellarini
Categories of Coalgebraic Games with Selective Sum, Fundamenta Informaticae, 134, 2014, 395--414, DOI 10.3233/FI-2014-1106.
[Abstract] [ pdf-copy]

F. Honsell, M. Lenisa, R. Redamalla
Equivalences and Congruences on Infinite Conway's Games, Theoretical Informatics and Applications, 46(2), 2012, 231--259.
[Abstract] [ pdf-copy]

F. Honsell, M. Lenisa
Conway's Games, algebraically and coalgebraically, Logical Methods in Computer Science, 7(3), 2011.
[Abstract] [ pdf-copy]

P. Di Gianantonio, F. Honsell, M. Lenisa
RPO, Second-order Contexts, and lambda-calculus, Logical Methods in Computer Science, 5(3), 2009.
[Abstract] [ pdf-copy]

P. Di Gianantonio, F. Honsell, M. Lenisa
A type assignment system for game semantics, Theoretical Computer Science, vol. 398, 2008, 150--169.
[Abstract] [ pdf-copy]

F. Honsell, M. Lenisa, R. Redamalla
Coalgebraic Description of Generalized Binary Methods, Mathematical Structures in Computer Science, vol. 17(4), 2007, 647--673.
[Abstract] [pdf-copy]

S. Abramsky, M. Lenisa
Linear realizability and full completeness for typed lambda calculi Annals of Pure and Applied Logic, vol. 134, 2005, pp. 122-168.
[Abstract] [pdf-copy]

M. Lenisa, J. Power, H. Watanabe
Category theory for operational semantics Theoretical Computer Science, Vol. 327, 2004, pp. 135-154.
[Abstract] [Compressed-pdf]

F. Honsell, M. Lenisa
Coinductive Characterizations of Applicative Structures Mathematical Structures in Computer Science, vol. 9, 1999, pp. 403-435.
[Abstract] [Compressed-ps]

F. Honsell, M. Lenisa
Semantical Analysis Of Perpetual Strategies In Lambda-Calculus Theoretical Computer Science, Vol. 212, 1999, pp. 183-209.
[Abstract] [Compressed-ps]

M. Forti, F. Honsell, M. Lenisa
An Axiomatization of partial n-place Operations, Mathematical Structures in Computer Science, vol. 7, 1997, pp. 283-302.
[Abstract] []

M. Forti, F. Honsell, M. Lenisa
Axiomatic Characterizations of Hyperuniverses and Applications, Annals of the New York Academy of Science, vol. 80, Papers on General Topology and Applications, 11th Summer Conference at the University of Southern Maine, , 1996, pp. 140-163.
[Abstract] [Compressed-ps]


Special volumes

F. Honsell, M. Lenisa, L. Liquori
A Framework for Defining Logical Frameworks, Special Volume in honour of Gordon Plotkin, L. Cardelli, M. Fiore, G. Winskel eds., ENTCS, 172,2007, 399--436.
[Abstract] [Soft-copy-pdf]

M. Forti, F. Honsell, M. Lenisa
Operations, Collections and Sets within a general Axiomatic Framework, Logic and Foundations of Mathematics, A. Cantini et al. eds., Kluwer Academic Publishers, 1999, 1--24
[] []

F. Honsell, M. Lenisa, U. Montanari, M. Pistore
Final Semantics for the pi-calculus, PROCOMET'98 Conference Proceedings, D. Gries et al. eds., Chapman & Hall, 1998, 225-243.
[Abstract] [Soft-copy-ps]


Proceedings of international Conferences

U. Dal Lago, F. Honsell, M. Lenisa, P. Pistone
On Quantitative Algebraic Higher-Order Theories, Proceedings of FSCD 2022 (7th International Conference on Formal Structures for Computation and Deduction), A. Felty ed., Leibniz International Proceedings in Informatics (LIPIcs),, 228, 2022, doi: 10.4230/LIPIcs.FSCD.2022.4
[Abstract and pdf-copy]

P. Di Gianantonio, M. Lenisa
Principal Types as Lambda Nets, Proceedings of TYPES 2021 (27th International Conference on Types for Proofs and Programs), H. Basold et al. eds., Leibniz International Proceedings in Informatics (LIPIcs), 239, 2022, doi:10.4230/LIPIcs.TYPES.2021.5
[Abstract and pdf-copy]

F. Honsell, M. Lenisa, I. Scagnetto
Lambda-symsym: an interactive Tool for playing with Involutions and Types, Proceedings of TYPES 2020 (26th International Conference on Types for Proofs and Programs), U. de' Liguoro et al. eds., Leibniz International Proceedings in Informatics (LIPIcs), 188, 2021, doi: 10.4230/LIPIcs.TYPES.2020.0
[Abstract] [pdf-copy]

A. Ciaffaglione,P. Di Gianantonio, F. Honsell, M. Lenisa, I. Scagnetto
Lambda!-calculus, intersection types, and involutions, Proceedings of FSCD 2019 (4th International Conference on Formal Structures for Computation and Deduction), H.Geuvers ed., Leibniz International Proceedings in Informatics (LIPIcs),, 131, 2019, doi: 10.4230/LIPIcs.FSCD.2019.15
[Abstract] [pdf-copy]

A. Ciaffaglione, F. Honsell, M. Lenisa, I. Scagnetto
The involutions-as-principal types/application-as-unification Analogy, Proceedings of LPAR-22 (22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning), Gilles Barthe, Geoff Sutcliffe and Margus Veanes eds., EPiC Series in Computing, 57, 2018, 254-270, EasyChair, doi:10.29007/ntwg
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, L. Liquori, I. Scagnetto
Implementing Cantor's Paradise, Proceedings of APLAS 2016, Chapter Programming Languages and Systems (APALS 2016), A. Igarashi ed., Springer LNCS, 10017, 2016, 229-250.
[Abstract] [pdf-copy]

M. Lenisa
Coalgebraic Multigames, Proceedings of the Workshop Coalgebraic Methods in Computer Science (CMCS 2014), M. Bonsangue ed., Springer LNCS, 8446, 2014, 33-49.
S[Abstract]R [pdf-copy]

P. Di Gianantonio, M. Lenisa
Innocent Game Semantics via Intersection Type Assignment Systems, CSL'2013 Conference Proceedings, S. Ronchi Della Rocca ed., LIPIcs Proceedings, 23, 2013, 231-247.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa
Unfixing the Fixpoint: the theories of the lambdaY-calculus, Proceedings in honor of Samsom Abramsky, B. Coecke, L. Ong. P. Panangaden eds., Springer LNCS, 7860, 2013, 150-165.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic, I. Scagnetto
LFP - A Logical Framework with External Predicates, LFMTP 2012 Workshop Proceedings, ACM Digital Library, 2012.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, R. Redamalla
Categories of Coalgebraic Games, MFCS 2012 Conference Proceedings, Springer LNCS, vol. 7464, 2012, 503-515.
[Abstract] [pdf-copy]

P. Di Gianantonio, Svetlana Jaksic, M. Lenisa
Efficient Bisimilarities from Second-order Reaction Semantics for pi-calculus, CONCUR 2010 Conference Proceedings, Springer LNCS, vol. 6269, 2010, 358-372.
[Abstract] [pdf-copy] [Extended version]

F. Honsell, M. Lenisa
Conway Games, coalgebraically, CALCO 2009 Conference Proceedings, Springer LNCS, vol. 5728, 2009, 300-316.
[Abstract] [pdf-copy] [Extended version]

P. Di Gianantonio, F. Honsell, M. Lenisa
Finitely Branching Labelled Transition Systems from Reaction Semantics for Process Calculi, WADT 2008 Conference Proceedings, Springer LNCS, vol. 5486, 2009.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, Luigi Liquori, Ivan Scagnetto
A Conditional Logical Framework, LPAR 2008 Conference Proceedings, Springer LNAI, vol. 5330, 2008 , 143-152.
[Abstract] [pdf-copy]

P. Di Gianantonio, F. Honsell, M. Lenisa
RPO, Second-order Contexts, and lambda-calculus, FoSSaCS 2008 Conference Proceedings, Springer LNCS, vol. 4962, 2008.
[Abstract] [pdf-copy]

D. Cancila, F. Honsell, M. Lenisa
Some Properties and Some Problems on Set Functors', Coalgebraic Methods in Computer Science CMCS'2006 Conference Proceedings, J. Adamek ed., ENTCS 164(1) , 2006, 67-84.
[Abstract] [pdf-copy]

D. Cancila, F. Honsell, M. Lenisa
Functors Determined by Values on Objects, MFPS XXII Conference Proceedings, S. Brookes and M. Mislove ed., ENTCS vol. 158 , 2006, 151-169.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, R. Redamalla
Coalgebraic Description of Generalized Binary Methods, Developments in Computational Models DCM'2005 Conference Proceedings, M. Fernandez et al eds., ENTCS vol. 135(3) , 2006, 73-84.
[Abstract] [pdf-copy]

R. Bruni, F. Honsell, M. Lenisa, M. Miculan
Modeling fresh names in the pi-calculus using abstractions, Coalgebraic Methods in Computer Science CMCS'2004 Conference Proceedings, J. Adamek ed., ENTCS vol. 106 , 2004, 25-41.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa
Wave-style Geometry of Interaction Models in Rel are Graph-like Lambda Models, TYPES'2003 Conference Proceedings, M. S. Berardi, M. Coppo, F. Damiani eds., Springer LNCS , vol. 3085, 2004 .
[Abstract] [Compressed-ps]

F. Honsell, M. Lenisa, R. Redamalla
Strict Geometry of Interaction Graph Models, LPAR'2003 Conference Proceedings, M. Vardi, A. Voronkov eds., Springer LNAI 2850 2003, pp. 403-417.
[Abstract] [Compressed-ps]

D. Cancila, F. Honsell, M. Lenisa
Generalized Coiteration Schemata, Coalgebraic Methods in Computer Science CMCS'2003 Conference Proceedings, P. Gumm ed., ENTCS vol. 82.1 , 2003.
[Abstract] [pdf-copy]

S. Abramsky, M. Lenisa
Fully Complete Minimal PER Models for the Simply Typed Lambda-calculus, CSL'2001 Conference Proceedings, Springer LNCS 2142 2001, pp. 443-457.
[Abstract] [Compressed-ps]

S. Abramsky, M. Lenisa
Axiomatizing Fully Complete Models for ML Polymorphic Types, MFCS'2000 Conference Proceedings M. Nielsen, B. Rovan eds., Springer LNCS vol. 1893, 2000, pp. 141-151.
[Abstract] [Compressed-ps]

S. Abramsky, M. Lenisa
A Fully-complete PER Model for ML Polymorphic Types, CSL'2000 Conference Proceedings, P. Clote, H.Schwichtenberg eds., Springer LNCS vol. 1862, 2000, pp. 140-155.
[Abstract] [Compressed-ps]

F. Honsell, M. Lenisa
Coalgebraic Coinduction in (Hyper)set-theoretic Categories, Coalgebraic Methods in Computer Science CMCS'2000 Conference Proceedings, B. Jacobs, J. Rutten eds., ENTCS vol. 33, 2000.
[Abstract] [Compressed-ps]

M. Lenisa, J. Power, H. Watanabe
Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads, Coalgebraic Methods in Computer Science CMCS'2000 Conference Proceedings, B. Jacobs, J. Rutten eds., ENTCS vol. 33, 2000.
[Abstract] [Compressed-ps]

M. Lenisa
From Set-theoretic Coinduction to Coalgebraic Coinduction: some results, some problems, Coalgebraic Methods in Computer Science CMCS'99 Conference Proceedings, B. Jacobs, J. Rutten eds., ENTCS vol. 19, 1999.
[Abstract] [Compressed-ps]

M. Lenisa
A Complete Coinductive Logical System for Bisimulation Equivalence of Circular Objects, FoSSaCS'99 (ETAPS) Conference Proceedings, W. Thomas ed., Springer LNCS vol. 1578, 1999.
[Abstract] [Compressed-ps]

M. Lenisa
Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for lambda-calculi TLCA'97 Conference Proceedings, P. de Groote, R. Hindley eds., Springer LNCS, vol. 1210, 1997, pp. 248-266.
[Abstract] [Compressed-ps]

M. Lenisa
A Uniform Syntactical Method for Proving Coinduction Principles in lambda-calculi, TAPSOFT'97 Conference Proceedings, M. Bidoit et al. eds., Springer LNCS, vol. 1214, 1997, pp. 309-320.
[Abstract] [Compressed-ps]

M. Lenisa
Final Semantics for a higher order concurrent langauage, CAAP'96 Conference Proceedings, H. Kirchner ed., Springer LNCS, vol. 1059, 1996, pp. 102-118.
[Abstract] [Compressed-ps]

F. Honsell, M. Lenisa
Final Semantics for untyped lambda-calculus, TLCA'95 Conference Proceedings, M. Dezani et al. eds., Springer LNCS, vol. 902, 1995, pp. 249-265.
[Abstract] [Compressed-ps]

M.Forti, F. Honsell, M. Lenisa
Processes and Hyperuniverses, MFCS'94 Conference Proceedings, I. Privara et al. eds., Springer LNCS, vol. 841, 1994, pp. 352-363.
[Abstract] [Compressed-ps]

F. Honsell, M. Lenisa
Some Results on Restricted lambda-calculi, MFCS'93 Conference Proceedings, A. Borzyszkowski et al. eds., Springer LNCS, vol. 711,1993, pp. 84-104.
[Abstract] [Compressed-ps]


Proceedings of Italian Conferences

D. Cancila, F. Honsell, M. Lenisa
Properties of Set Functors, COMETA'03 Conference Proceedings, F. Honsell et al. eds. , ENTCS, 104 , 2004, pp. 61-80.
[Abstract] [pdf file ]

F. Honsell, M. Lenisa, R. Redamalla
Coalgebraic Semantics and Observational Equivalences of an Imperative Class-based OO-language, COMETA'03 Conference Proceedings, F. Honsell et al. eds. , ENTCS, 104 , 2004, pp. 163-180.
[Abstract] [pdf file ]

R. Bruni, F. Honsell, M. Lenisa, M. Miculan
Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic, TOSCA'01 Conference Proceedings, M. Lenisa and M. Miculan eds., ENTCS, vol. 62. .
[Abstract] [Compressed-ps]


Technical Reports

F. Honsell, M. Lenisa
Polarized Multigames, TR 2013, Dipartimento di Matematica e Informatica, University of Udine (Italy), December 2013.
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa, R. Redamalla
Equivalences and Congruences on Infinite Conway's Games, TR 2011, Dipartimento di Matematica e Informatica, University of Udine (Italy), January 2011,
[Abstract] [pdf-copy]

F. Honsell, M. Lenisa
Coalgebraic Semantics of an Imperative Class Based Language, TR 02/2003, Dipartimento di Matematica e Informatica, University of Udine (Italy), January 2003,
[Abstract] [pdf-copy]

R. Bruni, F. Honsell, M. Lenisa, M. Miculan
Modeling Fresh Names in pi-calculus Using Abstractions, TR 21/2002, Dipartimento di Matematica e Informatica, University of Udine (Italy), April 2002, 17 pages.
[Abstract] [pdf-copy]

S. Abramsky, M. Lenisa
Fully-complete Models for ML Polymorphic Types, LFCS, University of Edinburgh, ECS-LFCS-99-414, October 1999, 49 pages.
[Abstract] [Compressed-ps]

M. Lenisa
From Set-theoretic Coinduction to Coalgebraic Coinduction: some results, some problems, Extended version of the paper in CMCS'99 Proc., October 1999.
[Abstract] [Compressed-ps]


PhD Thesis

M. Lenisa
Themes in Final Semantics, Dipartimento di Informatica, Universita` di Pisa, TD 6,March 1998.
[Abstract] [Compressed-ps]



Extended Abstracts

M. Lenisa
A Complete Coinductive Logical System for Bisimulation Equivalence of Circular Objects, extended abstract, in Proc. of the 1st Workshop of the Italian Project "Tecniche formali per la specifica, l'analisi, la verifica, la sintesi e la trasformazione di sistemi software", Roma, December 1998.
[Compressed-ps]

M. Lenisa
Fully Complete Models for ML Polymorphic Types, extended abstract, in Proc. of the Final Workshop of the Italian Project "Tecniche formali per la specifica, l'analisi, la verifica, la sintesi e la trasformazione di sistemi software", Venezia, January 2000.
[Compressed-ps]