A Conditional Logical Framework ⋆ (2009)
Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto
Abstract. The Conditional Logical Framework LFK is a variant of the Harper-Honsell-Plotkin’s Edinburgh Logical Framemork LF. It features a generalized form of λ-abstraction where β-reductions...
RPO, SECOND-ORDER CONTEXTS, AND λ-CALCULUS (2009)
Pietro Di Gianantonio, Furio Honsell, Marina Lenisa
Abstract. First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly...
RPO, Second-order Contexts, and Lambda-calculus (2009)
Di Gianantonio, Pietro, Honsell, Furio, Lenisa, Marina
First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly finitely...
An Abstract Notion of Application 1 (2008)
Pietro Di Gianantonio, Furio Honsell
Many concrete notions of function application, suitable for interpreting typed lambda calculi with recursive types, have been introduced in the literature. These arise in different fields such as set...
Kathleen Fisher, John C. Mitchell, Furio Honsell
Abstract. This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference...
Luigi Liquori, Furio Honsell, Rekha Redamalla
In this paper we develop the language theory underpinning the logical framework PLF. This language features lambda abstraction with patterns and application via pattern-matching. Reductions are...
www.elsevier.com/locate/entcs Some Properties and Some Problems on Set Functors 4 (2008)
Daniela Cancila, Furio Honsell, Marina Lenisa
We study properties of functors on categories of sets (classes) together with set (class) functions. In particular, we investigate the notion of inclusion preserving functor, and we discuss various...
CMCS 2004 Preliminary Version Modeling Fresh Names in the ss-calculus using Abstractions? (2008)
Furio Honsell, Marina Lenisa, Marino Miculan
Abstract In this paper, we model fresh names in the ss-calculus using abstractions with respect to a new binding operator `. Both the theory and the metatheory of the ss-calculus benefit from this...
Abstract CoMeta Project Workshop Preliminary Version Properties of Set Functors ⋆ (2008)
Daniela Cancila, Furio Honsell, Marina Lenisa
We prove that any endofunctor on a class-theoretic category has a final coalgebra. Moreover, we characterize functors on set-theoretic categories which are identical on objects, and functors which...
Roberto Bruni, Furio Honsell, Marina Lenisa, Marino Miculan
In this paper, we model fresh names in the π-calculus using abstractions with respect to a new binding operator θ. Both the theory and the metatheory of the π-calculus benefit from this simple...
Furio Honsell, Donald Sannella
We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Second Revised Edition. (2008)
Arnon Avron, Furio Honsell, Michael Barr, Charles Wells Toposes, Theories Springer
[4] Hengt Barendregt. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science. North-Holland, 1989.
Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, Ivan Scagnetto
The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In...
Nordic Journal of Computing Uncountable Limits and the Lambda Calculus (2008)
Pietro Di Gianantonio, Gordon Plotkin, Furio Honsell
Abstract. In this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the ω1-continuous function-space...
MFPS 2006 Functors Determined by Values on Objects 4 Abstract (2008)
Daniela Cancila, Furio Honsell, Marina Lenisa
Functors which are determined, up to natural isomorphism, by their values on objects, are called DVO (Defined by Values on Objects). We focus on the collection of polynomial functors on a category of...
Inverse Limit Models as Filter Models (2008)
Fabio Alessi, Mariangiola Dezani-ciancaglini, Furio Honsell
Natural intersection type preorders are the type structures which agree with the plain intuition of intersection type constructor as set-theoretic intersection operation and arrow type constructor as...
π-calculus in (Co)Inductive Type Theory (2008)
Furio Honsell, Marino Miculan, Ivan Scagnetto
We present a large and we think also significant case-study in computer assisted formal reasoning. We start by giving a higher order abstract syntax encoding of ß-calculus in the higher-order...
Game semantics for untyped fij-calculus (2007)
Pietro Di Gianantonio, Gianluca Franco, Furio Honsell
Abstract. We study extensional models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, somewhat unexpectedly and contrary to what happens in ordinary...
Furio Honsell, Marino Miculan, Ivan Scagnetto
We present a large and we think also significant case-study in computer assisted formal reasoning. We start by giving a higher order abstract syntax encoding of-calculus in the higher-order...
Fabio Alessi, Fabio Alessi, Paolo Baldan, Paolo Baldan, Furio Honsell, Furio Honsell
In this paper we introduce SFP
Operations, Collections and Sets within a General Axiomatic Framework (2007)
This paper is part of a general research programme on the Foundations of Mathematics, Logic and Computer Science, carried out since the early eighties at the the Seminar directed by Ennio De Giorgi...
Furio Honsell, Donald Sannella
We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Furio Honsell, Marino Miculan, Ivan Scagnetto
We present a large and we think also significant case-study in computer assisted formal reasoning. We start by giving a higher order abstract syntax encoding of-calculus in the higher-order...
TOSCA 2001 Preliminary Version (2007)
The Theory Of, Furio Honsell, Marino Miculan, Ivan Scagnetto
Syntax Furio Honsell and Marino Miculan and Ivan Scagnetto Dipartimento di Matematica e Informatica, Universita di Udine Via delle Scienze 206, 33100 Udine, Italy....
"Wave-style" Geometry of Interaction Models are Graph-like λ-models (2007)
We study the connections between graph models and "wavestyle " Geometry of Interaction (GoI) #-models. The latters arise when Abramsky's GoI construction, which generalizes...
Modeling Fresh Names in the π-calculus Using Abstractions (2007)
Roberto Bruni, Furio Honsell, Marina Lenisa, Marino Miculan
In this paper, we model fresh names in the π-calculus using abstractions w.r.t. a new binding operator θ. Both the theory and the metatheory of the π-calculus benefit from...
\Wave-style " Geometry of Interaction Models in Rel are Graph-like Lambda-models (2007)
Abstract. We study the connections between graph models and \wavestyle " Geometry of Interaction (GoI) -models. The latters arise when Abramsky's GoI axiomatization, which generalizes...
Furio Honsell, Marina Lenisa, Rekha Redamalla
Fickle is a class-based object oriented imperative language, which extends Java with object re-classification. In this paper, we introduce a natural observational equivalence over Fickle programs....
Furio Honsell, Rekha Redamalla
Abstract. We study a class of \wave-style " Geometry of Interaction (GoI) -models based on the category Rel of sets and relations. Wave GoI
Certified Reasoning on Real Numbers and Objects in Co-inductive Type Theory Candidate: (2007)
École Nationale, Supérieure Mines, Furio Honsell, Pietro Di Gianantonio, Claude Kirchner, Luigi Liquori, ...
In this thesis we adopt Formal Methods based on Type Theory for reasoning on the semantics of computer programs. The ultimate goal is their certification, that is, to prove that a fragment of...
Foundations for dynamic object re-classification (2007)
Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
We investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its own...
L' algoritmo del parcheggio (2007)
L' algoritmo del parcheggio, Furio Honsell, disegni di Bruno Bozzetto. . - Milano. NALUAF00001079, Mondadori. NAEDAF00003662. 2007.
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A Framework for Defining Logical Frameworks (2006)
Liquori, Luigi, Honsell, Furio, Lenisa, Marina
In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The...
A framework for defining logical frameworks (2006)
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
‡ Corresponding author. (2006)
Furio Honsell, Marina Lenisa, Rekha Redamalla, F. Honsell, M. Lenisa, R. Redamalla
We extend Reichel-Jacobs coalgebraic account of specification and refinement of objects and classes in Object Oriented Programming to (generalized) binary methods. These are methods that take more...
A framework for defining logical frameworks (2006)
Replace this file withprentcsmacro.sty for your meeting, or withentcsmacro.sty for your meeting. Both can be
A framework for defining logical frameworks (2006)
Thème Sym, Furio Honsell, Furio Honsell, Marina Lenisa, Marina Lenisa, Luigi Liquori, ...
apport de recherche SN 0249-6399 ISRN INRIA/RR--????--FR+ENG
Coalgebraic Description of Generalized Binary Methods (2005)
Furio Honsell, Marina Lenisa, Rekha Redamalla
We extend the Reichel-Jacobs coalgebraic account of specification and refinement of objects and classes in Object Oriented Programming to (generalized) binary methods. These are methods that take...
The need for formal methods for certifying the good behaviour of computer software is dramatically increasing with the growing complexity of the latter. Moreover, in the global computing framework...
Modeling Fresh Names in the π-calculus Using Abstractions (2004)
Roberto Bruni, Furio Honsell, Marina Lenisa, Marino Miculan
In this paper, we model fresh names in the #-calculus using abstractions with respect to a new binding operator #. Both the theory and the metatheory of the #-calculus benefit from this simple...
Generalized Coiteration Schemata (2003)
Daniela Cancila, Furio Honsell, Marina Lenisa
Coiterative functions can be explained categorically as final coalgebraic morphisms, once coinductive types are viewed as final coalgebras. However, the coiteration schema which arises in this way is...
Coalgebraic Semantics of an Imperative Class Based Language (2003)
We study two observational equivalences of Fickle programs. Fickle is a class-based object oriented imperative language...
Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic (2002)
Roberto Bruni, Furio Honsell, Marina Lenisa, Marino Miculan
In recent years, logical frameworks and tile logic have been separately proposed by our research groups, respectively in Udine and in Pisa, as suitable metalanguages with higher-order features for...
A category of compositional domain-models for separable (2001)
Stone Spaces, Fabio Alessi, Paolo Baldan, Furio Honsell
In this paper we introduce SFP M, a category of SFP domains which provides very satisfactory domain-models, i.e. “partializations”, of separable Stone spaces (2-Stone spaces). More specifically,...
π-calculus in (co)inductive type theory (2001)
Furio Honsell, Marino Miculan, Ivan Scagnetto
We present a large and we think also significant case-study in computer assisted formal reasoning. We start by giving a higher order abstract syntax encoding of π-calculus in the higher-order...
An axiomatic approach to metareasoning on nominal algebras in HOAS (2001)
Furio Honsell, Marino Miculan, Ivan Scagnetto
HOAS ⋆
Consistency of the Theory of Contexts (2001)
Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, Ivan Scagnetto
The Theory of Contexts is a type-theoretic axiomatization which has been recently proposed by some of the authors for giving a metalogical account of the fundamental notions of variable and context...
Approximation Theorems for Intersection Type Systems (2001)
Dezani-Ciancaglini, Mariangiola, Honsell, Furio, Motohama, Yoko
In this paper we prove that many intersection type theories of interest (including those which induce as filter models, Scott's and Park's D∞ models, the models studied in Barendregt Coppo Dezani,...
Coalgebraic Coinduction in (Hyper)set-theoretic Categories (2000)
Furio Honsell, Marina Lenisa, Honsell Lenisa
This paper is a contribution to the foundations of coinductive types and coiterative functions, in (Hyper)set-theoretical Categories, in terms of coalgebras. We consider atoms as first class...
Constructive Data Refinement in Typed Lambda Calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
. A new treatment of data refinement in typed lambda calculus is proposed, based on pre-logical relations [HS99] rather than logical relations as in [Ten94], and incorporating a constructive element....
Constructive Data Refinement in Typed Lambda Calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
. A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element....
Constructive data refinement in typed lambda calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
Abstract. A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive...
Furio Honsell, Donald Sannella
. We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful but having further algebraic properties...
Furio Honsell, Donald Sannella
. We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Furio Honsell And, Furio Honsell, Donald Sannella
. We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Furio Honsell And, Furio Honsell, Donald Sannella
. We study a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Furio Honsell, Donald Sannella
We study a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful as well as further algebraic properties...
Furio Honsell, Donald Sannella
. We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful but having further algebraic properties...
Furio Honsell, Donald Sannella
Abstract. We study a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful as well as further algebraic...
Furio Honsell, Donald Sannella
Abstract. We study a weakening of the notion of logical relations, called prelogical relations, that has many of the features that make logical relations so useful but having further algebraic...
Encoding modal logics in Logical Frameworks (1998)
Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deductionstyle proof systems for representing both...
A Lambda Calculus of Objects with Self-in Extension (1998)
Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
In this paper we investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its...
Encoding modal logics in Logical Frameworks (1998)
Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both...
Semantical Analysis of Perpetual Strategies in λ-calculus (1998)
this paper we carry out a semantical investigation of perpetual strategies in
Game Semantics for Untyped λβη-Calculus (1998)
Pietro Di Gianantonio, Gianluca Franco, Furio Honsell
. We study extensional models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, somewhat unexpectedly and contrary to what happens in ordinary categories...
Coinductive Characterizations of Applicative Structures (1998)
We discuss new ways of characterizing, as maximal fixed points of monotone operators, observational congruences on -terms and, more in general, equivalences on applicative structures. These...
A Lambda Calculus of Objects with Self-Inflicted Extension (1998)
Pietro Di Gianantonio, Furio Honsell, Luigi Liquori
In this paper we investigate, in the context of functional prototype-based languages, objects which might extend themselves upon receiving a message. The possibility for an object of extending its...
Encoding Modal Logics in Logical Frameworks (1997)
Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both...
Encoding Modal Logics in Logical Frameworks (1997)
Arnon Avron, Furio Honsell, Marino Miculan, Cristian Paravano
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both...
Axiomatic Characterizations of Hyperuniverses and Applications (1996)
Marco Forti, Furio Honsell, Marina Lenisa
Hyperuniverses are topological structures exhibiting strong closure properties under formation of subsets. They have been used both in Computer Science, for giving denotational semantics `a la...
A Natural Deduction Approach to Dynamic Logic (1996)
. Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as LEGO,...
Uncountable Limits and the Lambda Calculus (1995)
Di Gianantonio, Pietro, Honsell, Furio, Plotkin, Gordon
In this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the omega_1-continuous function-space...
Uncountable Limits and the Lambda Calculus (1995)
Di Gianantonio, Pietro, Honsell, Furio, Plotkin, Gordon
In this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the !1-continuous function-space...
A natural deduction approach to dynamic logics (1995)
Abstract. Natural Deduction style presentations of program logics are useful in view of the implementation of such logics in interactive proof development environments, based on type theory, such as...
Final Semantics for untyped λ-calculus (1995)
. Proof principles for reasoning about various semantics of untyped -calculus are discussed. The semantics are determined operationally by fixing a particular reduction strategy on -terms and a...
A lambda calculus of objects and method specialization (1994)
Kathleen Fisher, Computer Science Dept, Furio Honsell, John C. Mitchell
This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference system allows...
A lambda calculus of objects and method specialization (1994)
Kathleen Fisher, Computer Science Dept, Furio Honsell, John C. Mitchell
This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference system allows...
Processes and Hyperuniverses (1994)
Marco Forti, Furio Honsell, Marina Lenisa
. We show how to define domains of processes, which arise in the denotational semantics of concurrent languages, using hypersets, i.e. non-wellfounded sets. In particular we discuss how to solve...
A Lambda Calculus of Objects and Method Specialization (1994)
Kathleen Fisher, Computer Science Dept, Furio Honsell, John C. Mitchell
This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference system allows...
A Framework for Defining Logics (1993)
Plotkin, Gordon, Honsell, Furio, Harper, Robert
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent...
A Framework for Defining Logics (1993)
Plotkin, Gordon, Honsell, Furio, Harper, Robert
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent...
A framework for defining logics (1993)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed-calculus with dependent types....
Some Results on the Full Abstraction Problem for Restricted Lambda Calculi (1993)
ion Problem for Restricted Lambda Calculi Furio Honsell and Marina Lenisa Dipartimento di Matematica e Informatica, Universit`a di Udine, via Zanon,6 - Italy...
A Theory of Classes for a Functional Language with Effects (1993)
Furio Honsell, Ian A. Mason, Scott Smith, Carolyn Talcott
this paper we introduce a variable typed logic of effects (i.e. a logic of effects where classes can be defined and quantified over) inspired by the variable type systems of Feferman [3, 4] for...
A Variable Typed Logic of Effects (1993)
Furio Honsell, Ian A. Mason, Scott Smith, Carolyn Talcott
In this paper we introduce a variable typed logic of effects inspired by the variable type systems of Feferman for purely functional languages. VTLoE (Variable Typed Logic of Effects) is introduced...
Structured Operational Semantics of a fragment of the language Scheme (1993)
Furio Honsell, Alberto Pravato, Simona Ronchi, Della Rocca
In this paper we give a big-step structured operational semantics (SOS), in the style of Plotkin, Kahn and Milner, of a significant fragment of the functional programming language Scheme, including...
A framework for defining logics (1993)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent...
Using Typed Lambda Calculus to Implement Formal Systems on a Machine (1992)
Arnon Avron, Furio Honsell, Ian A. Mason, Robert Pollack
this paper and the LF. In particular the idea of having an operator T : Prop ! Type appears already in De Bruijn's earlier work, as does the idea of having several judgements. The paper [24]...
An Overview of the Edinburgh Logical Framework (1989)
Arnon Avron, Furio Honsell, Ian Mason
This paper serves as an introduction to the LF and summarizes the main points made in [1]. It is organized as follows. In section 2 we provide an outline of the LF specification language. This is...
A Framework for Defining Logics (1987)
Robert Harper, Furio Honsell, Gordon Plotkin
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus with dependent...
Partializing Stone Spaces using SFP domains
Fabio Alessi, Paolo Baldan, Furio Honsell
In this paper we investigate the problem of "partializing" Stone spaces by "Sequence of Finite Posets" (SFP) domains. More specifically, we introduce a suitable subcategory SFP m...