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. LenisaEfficient 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. LenisaConway Games, coalgebraically,
CALCO 2009 Conference Proceedings,
Springer LNCS, vol. 5728, 2009, 300-316.
[Abstract]
[pdf-copy]
[Extended version]
P. Di Gianantonio, F. Honsell,
M. LenisaFinitely 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. LenisaFunctors 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. LenisaPolarized Multigames,
TR 2013,
Dipartimento di Matematica e Informatica,
University of Udine (Italy), December 2013.
[Abstract]
[pdf-copy]
F. Honsell,
M. Lenisa, R. RedamallaEquivalences 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]