Comparison of the Axioms of Local and Global Universality. - Marco Forti; Furio Honsell (Math. Log. Q., 1984)

The Consistency of the Axiom of Universality for the Ordering of Cardinalities. - Marco Forti; Furio Honsell (J. Symb. Log., 1985)

A Model where Cardinal Ordering is Universal. - Marco Forti; Furio Honsell (Math. Log. Q., 1985)

A Natural Deduction treatment of Operational Semantics. - Rod M. Burstall; Furio Honsell (FSTTCS, 1988)

Reasoning About Interpretations in Qualitative λ-Models. - Furio Honsell; Simona Ronchi Della Rocca (Programming Concepts and Methods, 1990)

The lazy call-by-value Lamda-Calculus. - Lavinia Egidi; Furio Honsell; Simona Ronchi Della Rocca (MFCS, 1991)

A Theory of Classes for a Functional Language with Effects. - Furio Honsell; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (CSL, 1992)

Operational, denotational and logical descriptions: a case study. - Lavinia Egidi; Furio Honsell; Simona Ronchi Della Rocca (Fundam. Informaticae, 1992)

Using Typed Lambda Calculus to Implement Formal Systems on a Machine. - Arnon Avron; Furio Honsell; Ian A. Mason; Robert Pollack (J. Autom. Reason., 1992)

An Approximation Theorem for Topological Lambda Models and the Topological Incompleteness of Lambda Calculus. - Furio Honsell; Simona Ronchi Della Rocca (J. Comput. Syst. Sci., 1992)

Some Results on the Full Abstraction Problem for Restricted Lambda Calculi. - Furio Honsell; Marina Lenisa (MFCS, 1993)

An Abstract Notion of Application. - Pietro Di Gianantonio; Furio Honsell (TLCA, 1993)

Type Inference: Some Results, Some Problems. - Paola Giannini; Furio Honsell; Simona Ronchi Della Rocca (Fundam. Informaticae, 1993)

A Framework for Defining Logics. - Robert Harper 001; Furio Honsell; Gordon D. Plotkin (J. ACM, 1993)

Countable Non-Determinism and Uncountable Limits. - Pietro Di Gianantonio; Furio Honsell; Silvia Liani; Gordon D. Plotkin (CONCUR, 1994)

Processes and Hyperuniverses. - Michael Forti; Furio Honsell; Marina Lenisa (MFCS, 1994)

A lambda Calculus of Objects and Method Specialization. - Kathleen Fisher; Furio Honsell; John C. Mitchell (Nord. J. Comput., 1994)

Final Semantics for untyped lambda-calculus. - Furio Honsell; Marina Lenisa (TLCA, 1995)

A Natural Deduction Approach to Dynamic Logic. - Furio Honsell; Marino Miculan (TYPES, 1995)

Uncountable Limits and the lambda Calculus. - Pietro Di Gianantonio; Furio Honsell; Gordon D. Plotkin (Nord. J. Comput., 1995)

A Variable Typed Logic of Effects - Furio Honsell; Ian A. Mason; Scott F. Smith 001; Carolyn L. Talcott (Inf. Comput., 1995)

Choice Principles in Hyperuniverses. - Marco Forti; Furio Honsell (Ann. Pure Appl. Log., 1996)

A General Construction of Hyperuniverses. - Michael Forti; Furio Honsell (Theor. Comput. Sci., 1996)

Partializing Stone Spaces using SFP Domains (Extended Abstract). - Fabio Alessi; Paolo Baldan; Furio Honsell (TAPSOFT, 1997)

An Axiomatization of Partial n-Place Operations. - Marco Forti; Furio Honsell; Marina Lenisa (Math. Struct. Comput. Sci., 1997)

A Lambda Calculus of Objects with Self-Inflicted Extension. - Pietro Di Gianantonio; Furio Honsell; Luigi Liquori (OOPSLA, 1998)

Final semantics for the pi-calculus. - Furio Honsell; Marina Lenisa; Ugo Montanari; Marco Pistore (PROCOMET, 1998)

Addendum and Corrigendum: Choice Principles in Hyperuniverses. - Marco Forti; Furio Honsell (Ann. Pure Appl. Log., 1998)

Structured Operational Semantics of a Fragment of the Language Scheme. - Furio Honsell; Alberto Pravato; Simona Ronchi Della Rocca (J. Funct. Program., 1998)

Encoding Modal Logics in Logical Frameworks. - Arnon Avron; Furio Honsell; Marino Miculan; Cristian Paravano (Stud Logica, 1998)

Pre-logical Relations. - Furio Honsell; Donald Sannella (CSL, 1999)

Game Semantics for Untyped lambda beta eta-Calculus. - Pietro Di Gianantonio; Gianluca Franco; Furio Honsell (TLCA, 1999)

Coinductive characterizations of applicative structures. - Furio Honsell; Marina Lenisa (Math. Struct. Comput. Sci., 1999)

Semantical Analysis of Perpetual Strategies in lambda-Calculus. - Furio Honsell; Marina Lenisa (Theor. Comput. Sci., 1999)

Constructive Data Refinement in Typed Lambda Calculus. - Furio Honsell; John Longley; Donald Sannella; Andrzej Tarlecki (FoSSaCS, 2000)

A Complete Characterization of the Complete Intersection-Type Theories. - Mariangiola Dezani-Ciancaglini; Furio Honsell; Fabio Alessi (ICALP Satellite Workshops, 2000)

Compositional Characterizations of lambda-Terms Using Intersection Types. - Mariangiola Dezani-Ciancaglini; Furio Honsell; Yoko Motohama (MFCS, 2000)

Coalgebraic Coinduction in (Hyper)set-theoretic Categories. - Furio Honsell; Marina Lenisa (CMCS, 2000)

An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS. - Furio Honsell; Marino Miculan; Ivan Scagnetto (ICALP, 2001)

Filter Models and Easy Terms. - Fabio Alessi; Mariangiola Dezani-Ciancaglini; Furio Honsell (ICTCS, 2001)

Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic. - Roberto Bruni 001; Furio Honsell; Marina Lenisa; Marino Miculan (TOSCA, 2001)

The Theory of Contexts for First Order and Higher Order Abstract Syntax. - Furio Honsell; Marino Miculan; Ivan Scagnetto (TOSCA, 2001)

Approximation Theorems for Intersection Type Systems. - Mariangiola Dezani-Ciancaglini; Furio Honsell; Yoko Motohama (J. Log. Comput., 2001)

pi-calculus in (Co)inductive-type theory. - Furio Honsell; Marino Miculan; Ivan Scagnetto (Theor. Comput. Sci., 2001)

Prelogical Relations. - Furio Honsell; Donald Sannella (Inf. Comput., 2002)

A Coalgebraic Description of Web Interactions. - Daniela Cancila; Furio Honsell (ICTCS, 2003)

Strict Geometry of Interaction Graph Models. - Furio Honsell; Marina Lenisa; Rekha Redamalla (LPAR, 2003)

"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models. - Furio Honsell; Marina Lenisa (TYPES, 2003)

Mobility Types in Coq. - Furio Honsell; Ivan Scagnetto (TYPES, 2003)

Generalized Coiteration Schemata. - Daniela Cancila; Furio Honsell; Marina Lenisa (CMCS, 2003)

Properties of Set Functors. - Daniela Cancila; Furio Honsell; Marina Lenisa (COMETA, 2003)

Preface. - Furio Honsell; Marina Lenisa; Marino Miculan (COMETA, 2003)

Coalgebraic Semantics and Observational Equivalences of an Imperative Class-based OO-Language. - Furio Honsell; Marina Lenisa; Rekha Redamalla (COMETA, 2003)

A category of compositional domain-models for separable Stone spaces. - Fabio Alessi; Paolo Baldan; Furio Honsell (Theor. Comput. Sci., 2003)

A complete characterization of complete intersection-type preorders. - Mariangiola Dezani-Ciancaglini; Furio Honsell; Fabio Alessi (ACM Trans. Comput. Log., 2003)

Modeling Fresh Names in the π-calculus Using Abstractions. - Roberto Bruni 001; Furio Honsell; Marina Lenisa; Marino Miculan (CMCS, 2004)

Translating specifications from nominal logic to CIC with the theory of contexts. - Marino Miculan; Ivan Scagnetto; Furio Honsell (MERLIN, 2005)

A Language for Verification and Manipulation of Web Documents. - Luigi Liquori; Furio Honsell; Rekha Redamalla (WWV, 2005)

Coalgebraic Description of Generalized Binary Methods. - Furio Honsell; Marina Lenisa; Rekha Redamalla (DCM@ICALP, 2005)

A Language for Verification and Manipulation of Web Documents: (Extended Abstract). - Luigi Liquori; Furio Honsell; Rekha Redamalla (WWV, 2005)

Compositional characterisations of lambda-terms using intersection types. - Mariangiola Dezani-Ciancaglini; Furio Honsell; Yoko Motohama (Theor. Comput. Sci., 2005)

Functors Determined by Values on Objects. - Daniela Cancila; Furio Honsell; Marina Lenisa (MFPS, 2006)

Some Properties and Some Problems on Set Functors. - Daniela Cancila; Furio Honsell; Marina Lenisa (CMCS, 2006)

Consistency of the theory of contexts. - Anna Bucalo; Furio Honsell; Marino Miculan; Ivan Scagnetto; Martin Hofmann 001 (J. Funct. Program., 2006)

Editorial. - Furio Honsell; Carolyn L. Talcott (High. Order Symb. Comput., 2006)

A Framework for Defining Logical Frameworks. - Furio Honsell; Marina Lenisa; Luigi Liquori (Computation, Meaning, and Logic, 2007)

Coalgebraic description of generalised binary methods. - Furio Honsell; Marina Lenisa; Rekha Redamalla (Math. Struct. Comput. Sci., 2007)

A Conditional Logical Framework. - Furio Honsell; Marina Lenisa; Luigi Liquori; Ivan Scagnetto (LPAR, 2008)

Finitely Branching Labelled Transition Systems from Reaction Semantics for Process Calculi. - Pietro Di Gianantonio; Furio Honsell; Marina Lenisa (WADT, 2008)

A type assignment system for game semantics. - Pietro Di Gianantonio; Furio Honsell; Marina Lenisa (Theor. Comput. Sci., 2008)

Conway Games, Coalgebraically. - Furio Honsell; Marina Lenisa (CALCO, 2009)

RPO, Second-order Contexts, and Lambda-calculus - Pietro Di Gianantonio; Furio Honsell; Marina Lenisa (Log. Methods Comput. Sci., 2009)

On the completeness of order-theoretic models of the lambda-calculus. - Furio Honsell; Gordon D. Plotkin (Inf. Comput., 2009)

Conway games, algebraically and coalgebraically - Furio Honsell; Marina Lenisa (Log. Methods Comput. Sci., 2011)

Categories of Coalgebraic Games. - Furio Honsell; Marina Lenisa; Rekha Redamalla (MFCS, 2012)

Equivalences and Congruences on Infinite Conway Games. - Furio Honsell; Marina Lenisa; Rekha Redamalla (RAIRO Theor. Informatics Appl., 2012)

Unfixing the Fixpoint: The Theories of the λY-Calculus. - Furio Honsell; Marina Lenisa (Computation, Logic, Games, and Quantum Foundations, 2013)

25 years of formal proof cultures: some problems, some philosophy, bright future. - Furio Honsell (LFMTP, 2013)

L ax F: Side Conditions and External Evidence as Monads. - Furio Honsell; Luigi Liquori; Ivan Scagnetto (MFCS (1), 2014)

Categories of Coalgebraic Games with Selective Sum. - Furio Honsell; Marina Lenisa; Daniel Pellarini (Fundam. Informaticae, 2014)

Wherefore Art Thou... Semantics of Computation? - Furio Honsell (HaPoC, 2015)

Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (LFMTP, 2015)

Implementing Cantor's Paradise. - Furio Honsell; Marina Lenisa; Luigi Liquori; Ivan Scagnetto (APLAS, 2016)

An open logical framework. - Furio Honsell; Marina Lenisa; Ivan Scagnetto; Luigi Liquori; Petar Maksimovic 001 (J. Log. Comput., 2016)

LLF𝒫: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (Log. Methods Comput. Sci., 2017)

The Delta-Framework. - Furio Honsell; Luigi Liquori; Claude Stolze; Ivan Scagnetto (FSTTCS, 2018)

The involutions-as-principal types/application-as-unification Analogy. - Alberto Ciaffaglione; Furio Honsell; Marina Lenisa; Ivan Scagnetto (LPAR, 2018)

Linear lambda-calculus and Reversible Automatic Combinators. - Alberto Ciaffaglione; Furio Honsell; Marina Lenisa; Ivan Scagnetto (CoRR, 2018)

A prototype-based approach to object reclassification. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Luigi Liquori (CoRR, 2018)

Plugging-in proof development environments using Locks in LF. - Furio Honsell; Luigi Liquori; Petar Maksimovic 001; Ivan Scagnetto (Math. Struct. Comput. Sci., 2018)

Social robots as cultural objects: The sixth dimension of dynamicity? - Leopoldina Fortunati; Mauro Sarrica; Giovanni Ferrin; Sonia Brondi; Furio Honsell (Inf. Soc., 2018)

lambda!-calculus, Intersection Types, and Involutions. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa; Ivan Scagnetto (FSCD, 2019)

A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. - Fabio Alessi; Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa (LFMTP@LICS, 2019)

LF+ in Coq for "fast and loose" reasoning. - Fabio Alessi; Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Marina Lenisa; Ivan Scagnetto (J. Formaliz. Reason., 2019)

You need to show that you are not a robot. - Leopoldina Fortunati; Anna Maria Manganelli; Filippo Cavallo; Furio Honsell (New Media Soc., 2019)

Λ-Symsym: An Interactive Tool for Playing with Involutions and Types. - Furio Honsell; Marina Lenisa; Ivan Scagnetto (TYPES, 2020)

A protoype-based approach to object evolution. - Alberto Ciaffaglione; Pietro Di Gianantonio; Furio Honsell; Luigi Liquori (J. Object Technol., 2021)

On Quantitative Algebraic Higher-Order Theories. - Ugo Dal Lago; Furio Honsell; Marina Lenisa; Paolo Pistone (FSCD, 2022)

Two Views on Unification: Terms as Strategies. - Furio Honsell; Marina Lenisa; Ivan Scagnetto (FSTTCS, 2024)

Unsolvable Terms in Filter Models (Invited Talk). - Mariangiola Dezani-Ciancaglini; Paola Giannini; Furio Honsell (FSCD, 2025)

Principal types as partial involutions. - Furio Honsell; Marina Lenisa; Ivan Scagnetto (Math. Struct. Comput. Sci., 2025)