September 24th, 2019


Литература по семантике через теорию типов

Дмитрий Борисоглебский для своих штудий подготовил список статей о семантике через теории типов, но текст оказался слишком большим, чтобы поместиться в коммент. Так что я даю его тут отдельным постом (и спасибо Дмитрию!).

2019 A Topos-Based Approach to Building Language Ontologies
2019 Anatomy of a proposition
2019 Automorphisms of Types and Their Applications
2019 Automorphisms of types in certain type theories and representation of finite groups
2019 Knowledge representation and formal reasoning in ontologies with Coq
2019 Natural Language Semantics and Computability
2019 Practical subtyping for curry-style languages
2019 Representing Types as Neural Events
2018 A Type-Safe APProach to Identifying and Merging Changes in Complex Information Objects
2018 Collecting weighted coercions from crowd-sourced lexical data for compositional semantic analysis
2018 Handling verb phrase anaphora with dependent types and events
2018 On subtyping in type theories with canonical objects
2018 Particular types and particular dependence
2018 The Coinductive Formulation of Common Knowledge
2018 Theories as Types
2018 Type theory in the semantics of propositional attitudes
2018 Type-Theoretical foundations of the derivation system in Coq
2017 Adjectival and Adverbial Modification: The View from Modern Type Theories
2017 An analysis of selectional restrictions with dependent type semantics
2017 Collecting weighted coercions from crowd-sourced lexical data for compositional semantic analysis
2017 Composing criteria of individuation in copredication
2017 Dependent event types
2017 The essence of functional programming on semantic data
2017 Type-safe programming with OWL in Semantics4J
2016 A descriptive type foundation for RDF Schema
2016 A Dynamic Editor of Typed Data Transformations
2016 Adding agility to enterprise process and data engineering
2016 Challenges in the computational implementation of montagovian lexical semantics
2016 Contextualization and dependency in state-based modelling - application to event-B
2016 Frames as records
2016 Inquiry into RDF and OWL semantics
2016 Left Subsectivity: How to Infer that a Round Peg is Round
2016 Making explicit domain knowledge in formal system development
2016 Modeling co-verbal gesture perception in Type Theory with Records
2016 Proof assistants for natural language semantics
2016 Semantics with dependent types for indefinites
2016 Type-theoretic Means for Querying Heterogeneous Data Sources Available via Cloud APIs
2015 A type-theoretic approach to cloud data integration
2015 Computing the semantics of plurals and massive entities using many-sorted types
2015 Descriptive types for linked data resources
2015 Formal semantics for perceptual classification
2015 Minimal type inference for Linked Data consumers
2015 On isomorphism of dependent products in a typed logical framework
2015 Toward a type-theoretical approach for an ontologically-based detection of underground networks
2015 Towards modeling natural language inferences with part-whole relations using formal ontology and lexical semantics
2015 Towards the automated business process building by means of type theory
2015 Types, meanings and coercions in lexical semantics
2015 Using signatures in type theory to represent situations
2014 Adverbs in a modern type theory
2014 Definitional extension in type theory
2014 Deverbal Semantics and the Montagovian Generative Lexicon ΛTyn
2014 Formal semantics in modern type theories: Is it model-theoretic, proof-theoretic, or both?
2014 Modelling the semantic web using a type system
2014 Monotonicity reasoning in formal semantics based on modern type theories
2014 Natural Language Inference in Coq
2014 Small satellite systems design methodology: A formal and agile design process
2014 Specifying well-formed part-whole relations in Coq
2014 The montagovian generative lexicon λTyn: A type theoretical framework for natural language semantics
2014 Typed hilbert epsilon operators and the semantics of determiner phrases
2014 TyS - A framework to facilitate the implementation of object-oriented type checkers
2014 Using signatures in type theory to represent situations
2014 Vagueness and learning: A type-theoretic approach
2013 A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation
2013 A typed approach for contextualizing the part-whole relation
2013 Adjectives in a modern type-theoretical setting
2013 Coercive subtyping: Theory and implementation
2013 Definitional extension in type theory
2013 Formal foundations for situation awareness based on dependent type theory
2013 Logical polysemy and subtyping
2013 Modelling language, action, and perception in type theory with records
2013 Modeling ontological structures with type classes in Coq
2013 The montagovian generative lexicon λTyn: A type theoretical framework for natural language semantics
2012 A Constructive Type-Theoretical Formalism for the Interpretation of Subatomically Sensitive Natural Language Constructions
2012 A contextual type theory with judgemental modalities for reasoning from open assumptions
2012 A modal type theory for formalizing trusted communications
2012 A Type-Theoretical Approach for Ontologies: the Case of Roles
2012 An account of natural language coordination in type theory with coercive subtyping
2012 Common nouns as types
2012 Formal semantics in modern type theories with coercive subtyping
2012 Logical polysemy and subtyping
2012 Modelling language, action, and perception in type theory with records
2012 Type-theoretical dynamics: Exploring belief revision in a constructive framework
2012 Type Theory and Semantics in Flux
2012 Variable types for meaning assembly: A logical syntax for generic noun phrases introduced by most
2011 A focused sequent calculus framework for proof-search in pure type systems
2011 A single-type logic for natural language
2011 Contextual analysis of word meanings in type-theoretical semantics
2011 Copredication, quantification and frames
2011 Using a dependently-typed language for expressing ontologies
2011 Using formal methods with SysML in aerospace design and engineering
2010 A formal ontology for a computational approach of time and aspect
2010 Constructions for modeling product structure
2010 Four semantic layers of common nouns
2010 Frames in formal semantics
2010 Logic for modeling product structure
2010 Modeling Contexts with Dependent Types
2010 Towards a Type-Theoretical Account of Lexical Semantics
2010 Towards Ontological Correctness of Part-whole Relations with Dependent Types
2010 VeriML: Typed computation of logical terms inside a language with effects
2009 Meta-relation and ontology closure in conceptual structure theory
2009 Reasoning about relations with dependent types: Application to context-aware applications
2009 Towards an ontological modeling with dependent types: Application to part-whole relations
2008 A theorem prover with dependent types for reasoning about actions
2008 Causal reasoning with contexts using dependent types
2008 Towards a conceptual structure based on type theory
2008 Type theory with records and unification-based grammar
2007 An epistemic constructive definition of information
2007 Dependent record types for dynamic context representation
2007 Goal reasoning with context record types
2007 Interpreting metaphors in a new semantic theory of concept
2007 On the representation of imperative programs in a logical framework
2007 Using contexts to prove and share situations
2006 A sequent calculus for type theory
2005 Abstraction and ontology: Questions as propositional abstracts in type theory with records
2005 Austinian truth, attitudes and type theory
2005 Records and record types in semantic theory
2005 Situation semantics: The ontological balance sheet
2004 Ontological feedback in multiagent systems
2004 Types for Web Rule Languages: a preliminary study. Technical report A04-R-560
2003 A constructive approach to state description semantics
2003 Constructive semantics for extensional PTQ
2000 Formalizing Context in Intuitionistic Type Theory
1996 Type theoretic semantics for semnet
1995 Towards high-level deductive program synthesis based on type theory
1992 An implementation of the entity-relationship model in type theory
1991 Formal representation of semantic data models in type theory

UPDATE: обсуждение в чатике по типам --


Через пару часов на сутки вылетаю в Казань, буду рассказывать участникам очного этапа республиканского конкурса "Инженер года" ( про всякое и разное мышление.

А в четверг уже буду учиться работать с MS Teams, целый день (это я потихоньку двигаюсь в сторону реализации blended learning на базе идёй текста про PLM+CAD для образования --

Вьюнош сегодня вечером пойдёт на "Схематизацию на салфетке и в уме" (, а 27 сентября на "Онтологику 2.0" ( Не ЕГЭ единым (pun intended) жив человек.

2 октября 2019 в 19 часов будем презентовать трёхмесячный курс "Кругозор социальных танцев", Курс получается уникальный, я за лето написал в порядке создания его методики порядка 200 книжных страниц вот тут: Преподавать по вторникам-четвергам будут Ирина Парамонова (мультиданс) и Антон Климат (системный фитнес), а я там методолог. Заодно объявим о старте регулярных занятий по системному фитнесу по средам. Я, кстати, выяснил таки, почему социальный танец не выглядит таким уж трудным по сравнению с сольными танцами, но по факту там трудности не меньше. Проблема в точности: оказывается, для комфортного танца надо приходить в точку баланса на каждом шаге с точностью порядка 1см в момент порядка 0.1 секунды, причём не одному, а в паре ( Из моих личных достижений: используя методологию, я практически без занятий по танго пришёл на милонгу и станцевал там четыре танды -- две танго, одну танго-вальса и одну милонги. Нормально станцевал, метод работает!

В середине октября буду читать в ВШМ НИУ ВШЭ (практически армейские аббревиатуры!) восьмичасовой курс по машинному интеллекту для программы MBA. Рассказывать про машинный интеллект это как рассказывать про просто интеллект -- ничем ведь не отличается. А рассказ про интеллект (с упором на использование, конечно) это рассказ про человеческую цивилизацию. Вот как рассказать про человеческую (причём уже не совсем человеческую) цивилизацию за восемь часов? С учётом того, что рассказывать будущим MBA про устройство машинной части интеллекта всё равно что рассказывать про устройство мозга на всех его многочисленных системных уровнях. Но и не рассказывать, вроде, нельзя. Ибо будет впечатление, что интеллект, как булка, на деревьях растёт. Хотя и это отчасти верно: деревья решений в случайных лесах. Но оно им нужно, про это знать? Вот,, для самых новичков -- и мне кажется, что этого для MBA знать не нужно. Но вот про то, что сумма труда в мире не является константой, и поэтому машинный интеллект не может "отобрать работу" -- вот про это знать нужно. И ещё нужно знать про то, сколько стоит сегодня state-of-the-art машинного интеллекта (ой, много! но если не совсем state-of-the-art, то неожиданно дешевле грибов). И про многое другое, что нужно знать про человеков, если собираешься ими руководить. Многое нужно знать, но из устройства человеков нужно знать только то, что этому устройству нужно за работу адекватно платить и не урабатывать за эту оплату до смерти.