This article explores the role of conventions in the normalization of cocoa production in Ecuadorian Amazonia. Convention theory provides key theoretical tools for understanding coordination among agents. However, conventions must be understood as cultural constructions with a strong Eurocentric background that must be substantially modified in originally non-European contexts. A creative application of convention theory can partially overcome bifurcation among Western and non-Western rationalities. First, it shows that Western values and forms of coordination are heterogeneous, conflictive and opposing. Second, it (...) provides key insight for understanding the transformation of subaltern subjectivities generated from non-Western rationalities that are closely associated with subjugated knowledges. Third, in applying the concept of compromise, it allows one to understand cognitive hybridization and coordination among indigenous and Western agents and thus the complexities of processes of resistance, subversion and empowerment carried by indigenous communities. This article is focused on how cocoa production in Ecuadorian Amazonia serves as an example of the confluence and coordination of indigenous (using the concept of “Good Living” or Sumak Kawsay) and Western conventions. The assertion of Sumak Kawsay is understood as a relevant transformation of Ecuadorian post-colonial relations. It is shown that relevant industrial upgrading processes are justified by, among others, Sumak Kawsay repertoires. Additionally, dialogue on knowledge and compromise among conventions, and especially concerning Sumak Kawsay and the market, have been key facets shaping the development of a differentiated quality strand that has promoted relevant changes in the subaltern positioning of indigenous farmers in the cocoa commodity chain. (shrink)

We study the effect of scarcity on decision making by low income Swedes. We exploit the random assignment of welfare payments to study their borrowing decisions within the pawn and mainstream credit market. We document that higher educated borrowers borrow less frequently and choose lower loan to value ratios when their budget constraints are exogenously tighter. In contrast, low-educated borrowers do not respond to temporary elevated levels of scarcity. This lack of response translates into a significantly higher probability to default (...) and an 11.6% increase in borrowing cost. We show that a difference in access to liquidity and/or buffer stocks cannot explain our results. Instead a framework, where the awareness of self-control problems is positively correlated with education can explain that high-educated consumers choose a lower LTV as a commitment device to increase their likelihood to repay. Analogously, low-educated with less awareness of their future self-control problems, do not tie themselves to the mast and thus ignore the consequences of their credit decisions when focusing on solving acute liquidity problems. Our findings highlight that increased levels of scarcity risk reinforcing the conditions of poverty through overborrowing. (shrink)

La ciencia económica es una ciencia diversa, con innumerables escuelas y corrientes. En el presente texto se ordenan algunas de ellas tomando una serie de criterios epistemológicos de referencia. De esta forma se distingue en primer lugar entre economía estándar y economía política y, posteriormente dentro de esta última entre aproximaciones estructuralistas y post-estructuralistas. Dentro de este último grupo de reivindica la necesidad de construir una economía política desde el paradigma de la complejidad.

Biodiversity sciences witness a double dynamic. Whereas the need for interdisciplinary approaches is increasingly appreciated, most disciplinary studies are still confined to developing operational, discipline-specific indices. We show that a reassessment of the general notion of biodiversity is needed to clarify this situation. We advocate a new approach, according to which the main usefulness of this notion is not to capture quantitatively biological objects or processes, but to organize meaningful and coherent interdisciplinary interactions by constructively criticizing disciplinary studies. We apply (...) this approach to ecological-economic models, in the hope of launching more fruitful critical dialogs between economists and biologists. (shrink)

In this paper we propose a way to deal with natural language inference by implementing Modern Type Theoretical Semantics in the proof assistant Coq. The paper is a first attempt to deal with NLI and natural language reasoning in general by using the proof assistant technology. Valid NLIs are treated as theorems and as such the adequacy of our account is tested by trying to prove them. We use Luo’s Modern Type Theory with coercive subtyping as the formal language into (...) which we translate natural language semantics, and we further implement these semantics in the Coq proof assistant. It is shown that the use of a MTT with an adequate subtyping mechanism can give us a number of promising results as regards NLI. Specifically, it is shown that a number of inference cases, i.e. quantifiers, adjectives, conjoined noun phrases and temporal reference among other things can be successfully dealt with. It is then shown, that even though Coq is an interactive and not an automated theorem prover, automation of all of the test examples is possible by introducing user-defined automated tactics. Lastly, the paper offers a number of innovative approaches to NL phenomena like adjectives, collective predication, comparatives and factive verbs among other things, contributing in this respect to the theoretical study of formal semantics using MTTs. (shrink)

The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.

We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified (...) using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts. (shrink)

Ce matin-là, le coq chanta moins fort, et nettement plus faux. C'était au début de la 95e olympiade. Socrate était condamné à mort dans sa propre Cité. Figure magnétique de notre panthéon, Socrate est pourtant un être de la subversion et de l'inconvenance: il dit et fait des choses qui heurtent les institutions. Et c'est lui, dans sa bizarrerie, qui donne naissance à la philosophie. À travers le récit de sa dernière journée, Sandrine Alexandre donne vie à un Socrate en (...) décalage permanent avec les normes et les usages. Sous son égide, la philosophie ne peut être qu'une activité subversive. C'est cette dimension que retrouveront Nietzsche ou Foucault. Elle est ici restituée dans ce qui fait sa force et son originalité."--Page 4 of cover. (shrink)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to (...) term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11, 12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired (...) by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such as Coq and Agda (cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature. This paper provides a precise indication of this connection between homotopy theory and logic; a more detailed discussion of these and further results will be given in [20]. (shrink)

This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

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 truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed -calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO.

The article deals with an approach to the analysis of propositional attitudes based on the type-theoretical semantics proposed by A. Ranta and originating from the type theory of P. Martin-Löf. Type-theoretical semantics contains the notion of context and tools of extracting information from it in an explicit form. This allows us to correctly formalize the dependence on contexts typical of propositional attitudes. In the article the context is presented as a dependent sum type (Record type in the proof assistant Coq). (...) Ranta’s approach is refined and applied to the analysis of Quine’s phrase “Ralph believes that someone is a spy”. Three variants of formalization for this phrase are described which differ in the content of contextual knowledge and the way the truth values of the phrase are derived. Contexts are connected through the function of conversion, making it possible to relate truth values. As a result, it is shown that the instruments for working with contexts provided by type-theoretical semantics allow us to avoid the problem of opacity described by Quine. Provided formalization along with proofs is coded in Coq and made freely available. (shrink)

Le jour du Grand Pardon, présence du blanc, mon taleth immaculé, le seul taleth vierge de la famille,Comme les plumes des coqs et poules que Haim Aimé veut blanches pour le sacrifice d’avant Kippour,Le rabbin les égorge dans le jardin après les avoir tâtées sous l’aile en tenant le couteau entre les dents,puis passées au-dessus de nos têtes en prononçant nos noms, inoubliables bêtes blanches ensanglantées...

Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most well known and used in large-scale projects. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language (...) theory is of fundamental importance in the analysis, design, and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of contextfree grammars and languages. These include closure properties (union, concatenation, and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules, and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. As it turns out, this is a comprehensive formalization of the classical context-free language theory in the Coq proof assistant and includes the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction, and general enhancements of its libraries. (shrink)

Quelles lois Steven Cohen transgresse-t-il quand, le 10 septembre 2013, il réalise sa performance Coq / Cock sur la place du Trocadéro à Paris et est, en conséquence, condamné (sans peine) pour « exhibition sexuelle »? C’est la question que nous posons et la réponse ne se résume pas à des dispositions légales….

In this paper we present a study of adjectival/adverbial modification using modern type theories, i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented given their proof-theoretic nature. In MTT-semantics, common (...) nouns are interpreted as types rather than predicates. Therefore, in order to capture the semantics of adjectives adequately, one needs to meet the challenge of modeling CNs modified by adjectives as types. To explicate that this can be done successfully, we first look at the mainstream classification of adjectives, i.e. intersective, subsective and non-subsective adjectives. There, we show that the rich type structure available in MTTs, along with a suitable subtyping framework, offers an adequate mechanism to model these cases. In particular, this modelling naturally takes care of the characterising inferences associated with each class of adjectives. Then, more advanced issues on adjectival modification are discussed: degree adjectives, comparatives and multidimensional adjectives. There, it is shown that the use of indexed types can be usefully applied in order to deal with these cases. In the same vein, the issue of adverbial modification is discussed. We study two general typings for sentence and VP adverbs respectively. It is shown that the rich type structure in MTTs further provides useful organisational mechanisms in giving formal semantics for adverbs. In particular, we discuss the use of \-types to capture the veridicality/non-veridicality distinction and further discuss cases of intensional adverbs using the type theoretic notion of context. We also look at manner, subject and speech act adverbials and propose solutions using MTTs. Finally, we show that the current proof technology can help mechanically check the associated inferences. A number of our proposals concerning adjectival and adverbial modification have been formalised in the proof assistant Coq and many of the associated inference patterns are checked to be correctly captured. (shrink)

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

Lʹépistémologie peut-elle être autre chose que positive, une épistémologie matérialiste autre chose quʹun coq-à-lʹâne, et le matérialisme en épistémologie autre chose quʹun éléphant dans un magasin de porcelaine? Les études ici rassemblées apporteront peut-être quelques éléments de réflexion, tant historiques que théoriques, aidant à mettre en cause ces exclusives, interdits, et idées reçues. Elles fournissent en tout cas des aperçus multiples sur les thèses et problèmes épistémologiques intérieurs aux systèmes matérialistes, les droits et prétentions du matérialisme en épistémologie, la réalité (...) et la possibilité même dʹépistémologies matérialistes. -- Back cover. (shrink)

When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids. In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category (...) has for arrows triples →F)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\,\rightarrow \,F)$$\end{document} where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps makes them equal. In the second category the arrows are triples 2)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^2)$$\end{document} where R is a total functional relation between the subobjects F,F↪Σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$F, F \hookrightarrow \Sigma $$\end{document} of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category. (shrink)

RésuméSi on la compare avec l’habituelle coercition infligée au condamné à mort dans le monde romain, la peine réservée au parricide ne manque pas de surprendre par son originalité. Le coupable est chaussé de sabots de bois, sa tête est ensuite recouverte d’une cagoule en peau de loup et il sera ensuite flagellé à l’aide de verges sanguines. Pour finir, le contrevenant prend place dans un sac de cuir qui sera cousu après l’intromission d’un bestiaire composé d’un chien, d’un coq, (...) d’une vipère et d’un singe d’après la description donnée par Modestin au Digeste 48.9.9 pr., ceci avant que l’ensemble ne soit jeté à l’eau. Même si la symbolique précise de chaque élément est difficile à saisir en raison de leur origine diffuse, car issue de l’imagination populaire mêlée à divers substrats religieux imbriqués, cette procédure punitive forme un tout cohérent qui ne constitue pas un châtiment politisé au sens strict, c’est-à-dire déployé dans le cadre juridique de la cité. La justice humaine se borne surtout à établir la faute gravissime incombant au contrevenant, laquelle remet en cause le socle de l’organisation romaine, ainsi qu’à préparer son rejet total de la communauté humaine et du droit qui y standardise les rapports. En ce sens, l’homme se garde de donner directement la mort au parricide et la procédure d’expulsion n’est pas sans rappeler celle d’autres individus dits «monstrueux» parce que frappés d’anormalité physique, notamment sexuelle, car ceux-ci remettaient en cause le principe même de l’existence sociale. Cette priorité absolue que constitue la sauvegarde du groupe social dans le traitement du crime a pu servir de point d’ancrage à certaines positions contemporaines qui commandent d’extraire le contrevenant de l’ordre légal, afin de traiter efficacement un acte considéré comme abominable dans l’absolu. C’est l’exemple de la théorie du droit pénal de l’ennemi dont les lointaines racines peuvent être repérées dans les procédés d’expulsions socio-juridiques qui trouvaient à se déployer dans l’Antiquité romaine. (shrink)

We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics.

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called interactive theorem (...) provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we define two simple, one formal and the other informal, gate-level hardware description languages, design and develop a formal automatic combinational circuit equivalence checker tool, and test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables. CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course. (shrink)

We extend first-order logic to include variadic function symbols, and prove a substitution lemma. Two applications are given: one to bounded quantifier elimination and one to the definability of certain Borel sets.