Furio Honsell

CoRR, 2024

Two Views on Unification: Terms as Strategies.

[BibT_eX]

[DOI]

Proceedings of the 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2024

2022

On Quantitative Algebraic Higher-Order Theories.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

A protoype-based approach to object evolution.

[BibT_eX]

[DOI]

J. Object Technol., 2021

2020

Λ-Symsym: An Interactive Tool for Playing with Involutions and Types.

[BibT_eX]

[DOI]

Proceedings of the 26th International Conference on Types for Proofs and Programs, 2020

2019

You need to show that you are not a robot.

[BibT_eX]

[DOI]

Leopoldina Fortunati

Anna Maria Manganelli

Filippo Cavallo

New Media Soc., 2019

LF+ in Coq for "fast and loose" reasoning.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2019

A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2019

lambda!-calculus, Intersection Types, and Involutions.

[BibT_eX]

[DOI]

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

Social robots as cultural objects: The sixth dimension of dynamicity?

[BibT_eX]

[DOI]

Inf. Soc., 2018

Plugging-in proof development environments using Locks in LF.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2018

A prototype-based approach to object reclassification.

[BibT_eX]

[DOI]

CoRR, 2018

Linear lambda-calculus and Reversible Automatic Combinators.

[BibT_eX]

[DOI]

CoRR, 2018

The involutions-as-principal types/application-as-unification Analogy.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

The Delta-Framework.

[BibT_eX]

[DOI]

Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

2017

LLF𝒫: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

2016

An open logical framework.

[BibT_eX]

[DOI]

J. Log. Comput., 2016

Implementing Cantor's Paradise.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, 2015

Wherefore Art Thou... Semantics of Computation?

[BibT_eX]

[DOI]

Proceedings of the History and Philosophy of Computing - Third International Conference, 2015

2014

Categories of Coalgebraic Games with Selective Sum.

[BibT_eX]

[DOI]

Daniel Pellarini

Fundam. Informaticae, 2014

L ax F: Side Conditions and External Evidence as Monads.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2014, 2014

2013

25 years of formal proof cultures: some problems, some philosophy, bright future.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Unfixing the Fixpoint: The Theories of the λY-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky, 2013

2012

Equivalences and Congruences on Infinite Conway Games.

[BibT_eX]

[DOI]

RAIRO Theor. Informatics Appl., 2012

Categories of Coalgebraic Games.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2012, 2012

2011

Conway games, algebraically and coalgebraically

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

2009

On the completeness of order-theoretic models of the lambda-calculus.

[BibT_eX]

[DOI]

Inf. Comput., 2009

RPO, Second-order Contexts, and Lambda-calculus

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2009

Conway Games, Coalgebraically.

[BibT_eX]

[DOI]

Proceedings of the Algebra and Coalgebra in Computer Science, 2009

2008

A type assignment system for game semantics.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Finitely Branching Labelled Transition Systems from Reaction Semantics for Process Calculi.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Algebraic Development Techniques, 2008

A Conditional Logical Framework.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

2007

Coalgebraic description of generalised binary methods.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2007

A Framework for Defining Logical Frameworks.

[BibT_eX]

[DOI]

Proceedings of the Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, 2007

2006

Editorial.

[BibT_eX]

[DOI]

Carolyn L. Talcott

High. Order Symb. Comput., 2006

Consistency of the theory of contexts.

[BibT_eX]

[DOI]

J. Funct. Program., 2006

Some Properties and Some Problems on Set Functors.

[BibT_eX]

[DOI]

Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science, 2006

Functors Determined by Values on Objects.

[BibT_eX]

[DOI]

Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, 2006

2005

Compositional characterisations of lambda-terms using intersection types.

[BibT_eX]

[DOI]

Yoko Motohama

Theor. Comput. Sci., 2005

A Language for Verification and Manipulation of Web Documents: (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Automated Specification and Verification of Web Sites, 2005

Coalgebraic Description of Generalized Binary Methods.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Developments in Computational Models, 2005

A Language for Verification and Manipulation of Web Documents.

[BibT_eX]

Proceedings of the First International Workshop on Automated Specification and Verification of Web Sites (WWV 2005), 2005

Translating specifications from nominal logic to CIC with the theory of contexts.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Modeling Fresh Names in the ?-calculus Using Abstractions.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Coalgebraic Methods in Computer Science, 2004

2003

A complete characterization of complete intersection-type preorders.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2003

A category of compositional domain-models for separable Stone spaces.

[BibT_eX]

[DOI]

Paolo Baldan

Theor. Comput. Sci., 2003

Coalgebraic Semantics and Observational Equivalences of an Imperative Class-based OO-Language.

[BibT_eX]

[DOI]

Proceedings of the Workshop of the COMETA Project on Computational Metamodels, 2003

Preface.

[BibT_eX]

[DOI]

Proceedings of the Workshop of the COMETA Project on Computational Metamodels, 2003

Properties of Set Functors.

[BibT_eX]

[DOI]

Proceedings of the Workshop of the COMETA Project on Computational Metamodels, 2003

Generalized Coiteration Schemata.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Coalgebraic Methods in Computer Science, 2003

Mobility Types in Coq.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

Strict Geometry of Interaction Graph Models.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

A Coalgebraic Description of Web Interactions.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2002

Prelogical Relations.

[BibT_eX]

[DOI]

Donald Sannella

Inf. Comput., 2002

2001

pi-calculus in (Co)inductive-type theory.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

Approximation Theorems for Intersection Type Systems.

[BibT_eX]

[DOI]

Yoko Motohama

J. Log. Comput., 2001

The Theory of Contexts for First Order and Higher Order Abstract Syntax.

[BibT_eX]

[DOI]

Proceedings of the Theory of Concurrency, Higher Order Languages and Types, 2001

Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic.

[BibT_eX]

[DOI]

Proceedings of the Theory of Concurrency, Higher Order Languages and Types, 2001

Filter Models and Easy Terms.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 7th Italian Conference, 2001

An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 28th International Colloquium, 2001

2000

Coalgebraic Coinduction in (Hyper)set-theoretic Categories.

[BibT_eX]

[DOI]

Proceedings of the Coalgebraic Methods in Computer Science, 2000

Compositional Characterizations of lambda-Terms Using Intersection Types.

[BibT_eX]

[DOI]

Yoko Motohama

Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

A Complete Characterization of the Complete Intersection-Type Theories.

[BibT_eX]

Proceedings of the ICALP Workshops 2000, 2000

Constructive Data Refinement in Typed Lambda Calculus.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2000

1999

Semantical Analysis of Perpetual Strategies in lambda-Calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

Coinductive characterizations of applicative structures.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1999

Game Semantics for Untyped lambda beta eta-Calculus.

[BibT_eX]

[DOI]

Gianluca Franco

Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

Pre-logical Relations.

[BibT_eX]

[DOI]

Donald Sannella

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998

Encoding Modal Logics in Logical Frameworks.

[BibT_eX]

[DOI]

Stud Logica, 1998

Structured Operational Semantics of a Fragment of the Language Scheme.

[BibT_eX]

[DOI]

Alberto Pravato

J. Funct. Program., 1998

Addendum and Corrigendum: Choice Principles in Hyperuniverses.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1998

Final semantics for the pi-calculus.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

A Lambda Calculus of Objects with Self-Inflicted Extension.

[BibT_eX]

[DOI]

Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, 1998

1997

An Axiomatization of Partial n-Place Operations.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1997

Partializing Stone Spaces using SFP Domains (Extended Abstract).

[BibT_eX]

[DOI]

Paolo Baldan

Proceedings of the TAPSOFT'97: Theory and Practice of Software Development, 1997

1996

A General Construction of Hyperuniverses.

[BibT_eX]

[DOI]

Michael Forti

Theor. Comput. Sci., 1996

Choice Principles in Hyperuniverses.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1996

1995

A Variable Typed Logic of Effects

[BibT_eX]

[DOI]

Inf. Comput., May, 1995

Uncountable Limits and the lambda Calculus.

[BibT_eX]

Nord. J. Comput., 1995

A Natural Deduction Approach to Dynamic Logic.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1995

Final Semantics for untyped lambda-calculus.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1995

1994

A lambda Calculus of Objects and Method Specialization.

[BibT_eX]

Kathleen Fisher

John C. Mitchell

Nord. J. Comput., 1994

Processes and Hyperuniverses.

[BibT_eX]

[DOI]

Michael Forti

Proceedings of the Mathematical Foundations of Computer Science 1994, 1994

Countable Non-Determinism and Uncountable Limits.

[BibT_eX]

[DOI]

Silvia Liani

Proceedings of the CONCUR '94, 1994

1993

A Framework for Defining Logics.

[BibT_eX]

[DOI]

Robert Harper

J. ACM, 1993

Type Inference: Some Results, Some Problems.

[BibT_eX]

Paola Giannini

Fundam. Informaticae, 1993

An Abstract Notion of Application.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

Some Results on the Full Abstraction Problem for Restricted Lambda Calculi.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 1993, 1993

1992

An Approximation Theorem for Topological Lambda Models and the Topological Incompleteness of Lambda Calculus.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1992

Using Typed Lambda Calculus to Implement Formal Systems on a Machine.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

Operational, denotational and logical descriptions: a case study.

[BibT_eX]

Lavinia Egidi

Fundam. Informaticae, 1992

A Theory of Classes for a Functional Language with Effects.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 6th Workshop, 1992

1991

The lazy call-by-value Lamda-Calculus.

[BibT_eX]

[DOI]

Lavinia Egidi

Proceedings of the Mathematical Foundations of Computer Science 1991, 1991

1990

Reasoning About Interpretations in Qualitative λ-Models.

[BibT_eX]

Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990

1988

A Natural Deduction treatment of Operational Semantics.

[BibT_eX]

[DOI]

Rod M. Burstall

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1988

1985

A Model where Cardinal Ordering is Universal.

[BibT_eX]

[DOI]

Math. Log. Q., 1985

The Consistency of the Axiom of Universality for the Ordering of Cardinalities.

[BibT_eX]

[DOI]

J. Symb. Log., 1985

1984

Comparison of the Axioms of Local and Global Universality.

[BibT_eX]

[DOI]