Volume
LIPIcs, Volume 26
19th International Conference on Types for Proofs and Programs (TYPES 2013)
Event
TYPES 2013, April 22-26, 2013, Toulouse, FranceEditors
Publication Details
- published at: 2014-07-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-72-9
- DBLP: db/conf/types/types2013
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 26, TYPES'13, Complete Volume
Abstract
LIPIcs, Volume 26, TYPES'13, Complete Volume
Cite as
19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@Proceedings{matthes_et_al:LIPIcs.TYPES.2013,
title = {{LIPIcs, Volume 26, TYPES'13, Complete Volume}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013},
URN = {urn:nbn:de:0030-drops-46370},
doi = {10.4230/LIPIcs.TYPES.2013},
annote = {Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Conference Organization
Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as
19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{matthes_et_al:LIPIcs.TYPES.2013.i,
author = {Matthes, Ralph and Schubert, Aleksy},
title = {{Frontmatter, Table of Contents, Preface, Conference Organization}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {i--x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.i},
URN = {urn:nbn:de:0030-drops-46225},
doi = {10.4230/LIPIcs.TYPES.2013.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
Update Monads: Cointerpreting Directed Containers
Abstract
We introduce update monads as a generalization of state monads. Update
monads are the compatible compositions of reader and writer monads
given by a set and a monoid. Distributive laws between such monads are
given by actions of the monoid on the set.
We also discuss a dependently typed generalization of update monads. Unlike simple update monads, they cannot be factored into a reader and writer monad, but rather into similarly looking relative monads.
Dependently typed update monads arise from cointerpreting directed
containers, by which we mean an extension of an interpretation of the
opposite of the category of containers into the category of set
functors.
Cite as
Danel Ahman and Tarmo Uustalu. Update Monads: Cointerpreting Directed Containers. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ahman_et_al:LIPIcs.TYPES.2013.1,
author = {Ahman, Danel and Uustalu, Tarmo},
title = {{Update Monads: Cointerpreting Directed Containers}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {1--23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.1},
URN = {urn:nbn:de:0030-drops-46235},
doi = {10.4230/LIPIcs.TYPES.2013.1},
annote = {Keywords: monads and distributive laws, reader, writer and state monads, monoids and monoid actions, directed containers}
}
Document
A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Abstract
We propose a very simple modification of Kreisel's modified realizability in order to computationally realize Markov's Principle in the context of Heyting Arithmetic. Intuitively, realizers correspond to arbitrary strategies in Hintikka-Tarski games, while in Kreisel's realizability they can only represent winning strategies. Our definition, however, does not employ directly game semantical concepts and remains in the style of functional interpretations. As term calculus, we employ a purely functional language, which is Goedel's System T enriched with some syntactic sugar.
Cite as
Federico Aschieri and Margherita Zorzi. A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 24-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{aschieri_et_al:LIPIcs.TYPES.2013.24,
author = {Aschieri, Federico and Zorzi, Margherita},
title = {{A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {24--44},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.24},
URN = {urn:nbn:de:0030-drops-46245},
doi = {10.4230/LIPIcs.TYPES.2013.24},
annote = {Keywords: Markov's Principle, Intuitionistic Realizability, Heyting Arithmetic, Game Semantics}
}
Document
Formally Verified Implementation of an Idealized Model of Virtualization
Abstract
VirtualCert is a machine-checked model of virtualization that can be
used to reason about isolation between operating systems in presence
of cache-based side-channels. In contrast to most prominent projects
on operating systems verification, where such guarantees are proved
directly on concrete implementations of hypervisors, VirtualCert
abstracts away most implementations issues and specifies the effects
of hypervisor actions axiomatically, in terms of preconditions and
postconditions. Unfortunately, seemingly innocuous implementation
issues are often relevant for security. Incorporating the treatment of
errors into VirtualCert is therefore an important step towards
strengthening the isolation theorems proved in earlier work. In this
paper, we extend our earlier model with errors, and prove that
isolation theorems still apply. In addition, we provide an executable specification of the hypervisor, and prove that it correctly implements the axiomatic model. The executable specification constitutes a first step towards a more realistic implementation of a hypervisor, and provides a useful tool for validating the axiomatic semantics developed in previous work.
Cite as
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally Verified Implementation of an Idealized Model of Virtualization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 45-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{barthe_et_al:LIPIcs.TYPES.2013.45,
author = {Barthe, Gilles and Betarte, Gustavo and Campo, Juan Diego and Chimento, Jes\'{u}s Mauricio and Luna, Carlos},
title = {{Formally Verified Implementation of an Idealized Model of Virtualization}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {45--63},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.45},
URN = {urn:nbn:de:0030-drops-46254},
doi = {10.4230/LIPIcs.TYPES.2013.45},
annote = {Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation}
}
Document
Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic
Abstract
We produce a first order proof of a famous combinatorial result, Ramsey Theorem for pairs and in two colors. Our goal is to find the minimal classical principle that implies the "miniature" version of Ramsey we may express in Heyting Arithmetic HA. We are going to prove that Ramsey Theorem for pairs with recursive assignments of two colors is equivalent in HA to the sub-classical principle Sigma-0-3-LLPO. One possible application of our result could be to use classical realization to give constructive proofs of some combinatorial corollaries of Ramsey; another, a formalization of Ramsey in HA, using a proof assistant. In order to compare Ramsey Theorem with first order classical principles, we express it as a schema in the first order language of arithmetic, instead of using quantification over sets and functions as it is more usual: all sets we deal with are explicitly defined as arithmetical predicates. In particular, we formally define the homogeneous set which is the witness of Ramsey theorem as a Delta-0-3-arithmetical predicate.
Cite as
Stefano Berardi and Silvia Steila. Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 64-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{berardi_et_al:LIPIcs.TYPES.2013.64,
author = {Berardi, Stefano and Steila, Silvia},
title = {{Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {64--83},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.64},
URN = {urn:nbn:de:0030-drops-46269},
doi = {10.4230/LIPIcs.TYPES.2013.64},
annote = {Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem}
}
Document
Extracting Imperative Programs from Proofs: In-place Quicksort
Abstract
The process of program extraction is primarily associated with
functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability
interpretation to extract a program from the proof. Using monads we
are able to exhibit the inherent imperative nature of the extracted
program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.
Cite as
Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods. Extracting Imperative Programs from Proofs: In-place Quicksort. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 84-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{berger_et_al:LIPIcs.TYPES.2013.84,
author = {Berger, Ulrich and Seisenberger, Monika and Woods, Gregory J. M.},
title = {{Extracting Imperative Programs from Proofs: In-place Quicksort}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {84--106},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.84},
URN = {urn:nbn:de:0030-drops-46274},
doi = {10.4230/LIPIcs.TYPES.2013.84},
annote = {Keywords: Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort,Computational Monads, Minlog}
}
Document
A Model of Type Theory in Cubical Sets
Abstract
We present a model of type theory with dependent product, sum, and
identity, in cubical sets. We describe a universe and explain how
to transform an equivalence between two types into an equality. We
also explain how to model propositional truncation and the circle.
While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
Cite as
Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 107-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{bezem_et_al:LIPIcs.TYPES.2013.107,
author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
title = {{A Model of Type Theory in Cubical Sets}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {107--128},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107},
URN = {urn:nbn:de:0030-drops-46284},
doi = {10.4230/LIPIcs.TYPES.2013.107},
annote = {Keywords: Models of dependent type theory, cubical sets, Univalent Foundations}
}
Document
Isomorphism of "Functional" Intersection Types
Abstract
Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.
Cite as
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of "Functional" Intersection Types. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 129-149, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{coppo_et_al:LIPIcs.TYPES.2013.129,
author = {Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Margaria, Ines and Zacchi, Maddalena},
title = {{Isomorphism of "Functional" Intersection Types}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {129--149},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.129},
URN = {urn:nbn:de:0030-drops-46296},
doi = {10.4230/LIPIcs.TYPES.2013.129},
annote = {Keywords: Type Isomorphism, Lambda calculus, Intersection Types}
}
Document
A Hybrid Linear Logic for Constrained Transition Systems
Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
Cite as
Joëlle Despeyroux and Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 150-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{despeyroux_et_al:LIPIcs.TYPES.2013.150,
author = {Despeyroux, Jo\"{e}lle and Chaudhuri, Kaustuv},
title = {{A Hybrid Linear Logic for Constrained Transition Systems}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {150--168},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.150},
URN = {urn:nbn:de:0030-drops-46302},
doi = {10.4230/LIPIcs.TYPES.2013.150},
annote = {Keywords: Linear logic, hybrid logic, stochastic pi-calculus, focusing, adequacy}
}
Document
The Rooster and the Syntactic Bracket
Abstract
We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary restrictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive constructions on which the Coq proof assistant is an implementation.
Cite as
Hugo Herbelin and Arnaud Spiwack. The Rooster and the Syntactic Bracket. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 169-187, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{herbelin_et_al:LIPIcs.TYPES.2013.169,
author = {Herbelin, Hugo and Spiwack, Arnaud},
title = {{The Rooster and the Syntactic Bracket}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {169--187},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.169},
URN = {urn:nbn:de:0030-drops-46318},
doi = {10.4230/LIPIcs.TYPES.2013.169},
annote = {Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families}
}
Document
A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators
Abstract
First, we reconstruct Wim Veldman's result that Open Induction on Cantor space can be derived from Double-negation Shift and Markov's Principle. In doing this, we notice that one has to use a countable choice axiom in the proof and that Markov's Principle is replaceable by slightly strengthening the Double-negation Shift schema. We show that this strengthened version of Double-negation Shift can nonetheless be derived in a constructive intermediate logic based on delimited control operators, extended with axioms for higher-type Heyting Arithmetic. We formalize the argument and thus obtain a proof term that directly derives Open Induction on Cantor space by the shift and reset delimited control operators of Danvy and Filinski.
Cite as
Danko Ilik and Keiko Nakata. A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 188-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{ilik_et_al:LIPIcs.TYPES.2013.188,
author = {Ilik, Danko and Nakata, Keiko},
title = {{A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {188--201},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.188},
URN = {urn:nbn:de:0030-drops-46320},
doi = {10.4230/LIPIcs.TYPES.2013.188},
annote = {Keywords: Open Induction, Axiom of Choice, Double Negation Shift, Markov's Principle, delimited control operators}
}
Document
The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics
Abstract
We present a framework, named the Montagovian generative lexicon, for computing the semantics of natural language sentences, expressed in many sorted higher order logic. Word meaning is depicted by several lambda terms of second order lambda calculus (Girard's system F): the principal lambda term encodes the argument structure, while the other lambda terms implement meaning transfers. The base types include a type for propositions and many types for sorts of a many sorted logic for expressing restriction of selection. This framework is able to integrate a proper treatment of lexical phenomena into a Montagovian compositional semantics, like the (im)possible arguments of a predicate, and the adaptation of a word meaning to some contexts. Among these adaptations of a word's sense to the context, ontological inclusions are handled by coercive subtyping, an extension of system F introduced in the present paper. The benefits of this framework for lexical semantics and pragmatics are illustrated on meaning transfers and coercions, on possible and impossible copredication over different senses, on deverbal ambiguities, and on "fictive motion". Next we show that the compositional treatment of determiners, quantifiers, plurals,... are finer grained in our framework. We then conclude with the linguistic, logical and computational perspectives opened by the Montagovian generative lexicon.
Cite as
Christian Retoré. The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 202-229, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{retore:LIPIcs.TYPES.2013.202,
author = {Retor\'{e}, Christian},
title = {{The Montagovian Generative Lexicon Lambda Ty\underlinen: a Type Theoretical Framework for Natural Language Semantics}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {202--229},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.202},
URN = {urn:nbn:de:0030-drops-46336},
doi = {10.4230/LIPIcs.TYPES.2013.202},
annote = {Keywords: type theory, computational linguistics}
}
Document
A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language
Abstract
In this paper we present a compiler that translates programs from an
imperative higher-order language into a sequence of instructions
for an abstract machine. We consider an extension of the Krivine machine for the call-by-name lambda calculus, which includes strict operators and imperative features. We show that the compiler is
correct with respect to the big-step semantics of our language, both
for convergent and divergent programs.
Cite as
Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano. A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 230-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{rodriguez_et_al:LIPIcs.TYPES.2013.230,
author = {Rodr{\'\i}guez, Leonardo and Fridlender, Daniel and Pagano, Miguel},
title = {{A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {230--250},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.230},
URN = {urn:nbn:de:0030-drops-46343},
doi = {10.4230/LIPIcs.TYPES.2013.230},
annote = {Keywords: Abstract Machines, Compiler Correctness, Big-step semantics}
}
Document
Definitional Extension in Type Theory
Abstract
When we extend a type system, the relation between the original system and its extension is an important issue we want to know. Conservative extension is a traditional relation we study with. But in some cases, like coercive subtyping, it is not strong enough to capture all the properties, more powerful relation between the systems is required. We bring the idea definitional extension from mathematical logic into type theory. In this paper, we study the notion of definitional extension for type theories and explicate its use, both informally and formally, in the context of coercive subtyping.
Cite as
Tao Xue. Definitional Extension in Type Theory. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 251-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
Copy BibTex To Clipboard
@InProceedings{xue:LIPIcs.TYPES.2013.251,
author = {Xue, Tao},
title = {{Definitional Extension in Type Theory}},
booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
pages = {251--269},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-72-9},
ISSN = {1868-8969},
year = {2014},
volume = {26},
editor = {Matthes, Ralph and Schubert, Aleksy},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.251},
URN = {urn:nbn:de:0030-drops-46352},
doi = {10.4230/LIPIcs.TYPES.2013.251},
annote = {Keywords: conservative extension, definitional extension, subtype, coercive subtyping}
}