?

Log in

No account? Create an account
Лабораторный журнал -- Day [entries|friends|calendar]
Anatoly Levenchuk

[ website | Лабораторный журнал ]
[ userinfo | livejournal userinfo ]
[ calendar | livejournal calendar ]

Литература по семантике через теорию типов [24 Sep 2019|12:54pm]
Дмитрий Борисоглебский для своих штудий подготовил список статей о семантике через теории типов, но текст оказался слишком большим, чтобы поместиться в коммент. Так что я даю его тут отдельным постом (и спасибо Дмитрию!).

2019 A Topos-Based Approach to Building Language Ontologies https://link.springer.com/chapter/10.1007%2F978-3-662-59648-7_2
2019 Anatomy of a proposition https://link.springer.com/article/10.1007%2Fs11229-017-1512-y
2019 Automorphisms of Types and Their Applications https://link.springer.com/article/10.1007%2Fs10958-019-04386-8
2019 Automorphisms of types in certain type theories and representation of finite groups https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/automorphisms-of-types-in-certain-type-theories-and-representation-of-finite-groups/7370BD6B69583FA648B3E9BB82766E86
2019 Knowledge representation and formal reasoning in ontologies with Coq https://link.springer.com/chapter/10.1007%2F978-3-319-91008-6_74
2019 Natural Language Semantics and Computability https://link.springer.com/article/10.1007%2Fs10849-019-09290-7
2019 Practical subtyping for curry-style languages https://dl.acm.org/citation.cfm?doid=3299867.3285955
2019 Representing Types as Neural Events https://link.springer.com/article/10.1007%2Fs10849-019-09285-4
2018 A Type-Safe APProach to Identifying and Merging Changes in Complex Information Objects https://www.sciencedirect.com/science/article/pii/S1877050918323949?via%3Dihub
2018 Collecting weighted coercions from crowd-sourced lexical data for compositional semantic analysis https://link.springer.com/chapter/10.1007%2F978-3-319-93794-6_15
2018 Handling verb phrase anaphora with dependent types and events https://link.springer.com/chapter/10.1007%2F978-3-662-57669-4_12
2018 On subtyping in type theories with canonical objects http://drops.dagstuhl.de/opus/volltexte/2018/9849/
2018 Particular types and particular dependence http://ebooks.iospress.nl/publication/50242
2018 The Coinductive Formulation of Common Knowledge https://link.springer.com/chapter/10.1007%2F978-3-319-94821-8_8
2018 Theories as Types https://link.springer.com/chapter/10.1007%2F978-3-319-94205-6_38
2018 Type theory in the semantics of propositional attitudes https://www.pdcnet.org/eps/content/eps_2018_0055_0004_0026_0037
2018 Type-Theoretical foundations of the derivation system in Coq https://ieeexplore.ieee.org/document/8516885/
2017 Adjectival and Adverbial Modification: The View from Modern Type Theories https://link.springer.com/article/10.1007%2Fs10849-017-9246-2
2017 An analysis of selectional restrictions with dependent type semantics https://link.springer.com/chapter/10.1007%2F978-3-319-61572-1_2
2017 Collecting weighted coercions from crowd-sourced lexical data for compositional semantic analysis https://link.springer.com/chapter/10.1007%2F978-3-319-93794-6_15
2017 Composing criteria of individuation in copredication https://academic.oup.com/jos/article-abstract/34/2/333/2555474?redirectedFrom=fulltext
2017 Dependent event types https://link.springer.com/chapter/10.1007%2F978-3-662-55386-2_15
2017 The essence of functional programming on semantic data https://link.springer.com/chapter/10.1007%2F978-3-662-54434-1_28
2017 Type-safe programming with OWL in Semantics4J http://ceur-ws.org/Vol-1963/paper549.pdf
2016 A descriptive type foundation for RDF Schema https://www.sciencedirect.com/science/article/pii/S2352220816300037?via%3Dihub
2016 A Dynamic Editor of Typed Data Transformations https://www.sciencedirect.com/science/article/pii/S187705091631883X?via%3Dihub
2016 Adding agility to enterprise process and data engineering http://www.iiis.org/CDs2016/CD2016Spring/papers/ZA878YI.pdf
2016 Challenges in the computational implementation of montagovian lexical semantics https://link.springer.com/chapter/10.1007%2F978-3-319-61572-1_7
2016 Contextualization and dependency in state-based modelling - application to event-B https://link.springer.com/chapter/10.1007%2F978-3-319-66854-3_11
2016 Frames as records https://link.springer.com/chapter/10.1007%2F978-3-662-53042-9_1
2016 Inquiry into RDF and OWL semantics https://link.springer.com/chapter/10.1007%2F978-3-319-50112-3_2
2016 Left Subsectivity: How to Infer that a Round Peg is Round https://onlinelibrary.wiley.com/doi/abs/10.1111/1746-8361.12159
2016 Making explicit domain knowledge in formal system development https://www.sciencedirect.com/science/article/pii/S0167642315004153?via%3Dihub
2016 Modeling co-verbal gesture perception in Type Theory with Records https://annals-csis.org/proceedings/2016/drp/83.html
2016 Proof assistants for natural language semantics https://link.springer.com/chapter/10.1007%2F978-3-662-53826-5_6
2016 Semantics with dependent types for indefinites https://content.sciendo.com/view/journals/slgr/46/1/article-p173.xml
2016 Type-theoretic Means for Querying Heterogeneous Data Sources Available via Cloud APIs https://linkinghub.elsevier.com/retrieve/pii/S1877050916318786
2015 A type-theoretic approach to cloud data integration http://www.scitepress.org/DigitalLibrary/Link.aspx?doi=10.5220/0005495301640169
2015 Computing the semantics of plurals and massive entities using many-sorted types https://link.springer.com/chapter/10.1007%2F978-3-662-48119-6_11
2015 Descriptive types for linked data resources https://link.springer.com/chapter/10.1007%2F978-3-662-46823-4_1
2015 Formal semantics for perceptual classification https://academic.oup.com/logcom/article-abstract/25/2/335/954129?redirectedFrom=fulltext
2015 Minimal type inference for Linked Data consumers https://www.sciencedirect.com/science/article/pii/S2352220814001011?via%3Dihub
2015 On isomorphism of dependent products in a typed logical framework http://drops.dagstuhl.de/opus/volltexte/2015/5501/
2015 Toward a type-theoretical approach for an ontologically-based detection of underground networks https://link.springer.com/chapter/10.1007%2F978-3-319-25159-2_8
2015 Towards modeling natural language inferences with part-whole relations using formal ontology and lexical semantics http://ceur-ws.org/Vol-1517/JOWO-15_FOfAI_paper_6.pdf
2015 Towards the automated business process building by means of type theory https://dl.acm.org/citation.cfm?doid=2723839.2723847
2015 Types, meanings and coercions in lexical semantics https://www.sciencedirect.com/science/article/pii/S0024384115000029?via%3Dihub
2015 Using signatures in type theory to represent situations https://link.springer.com/chapter/10.1007%2F978-3-662-48119-6_13
2014 Adverbs in a modern type theory https://link.springer.com/chapter/10.1007%2F978-3-662-43742-1_4
2014 Definitional extension in type theory http://drops.dagstuhl.de/opus/volltexte/2014/4635/
2014 Deverbal Semantics and the Montagovian Generative Lexicon ΛTyn https://link.springer.com/article/10.1007%2Fs10849-014-9187-y
2014 Formal semantics in modern type theories: Is it model-theoretic, proof-theoretic, or both? https://link.springer.com/chapter/10.1007%2F978-3-662-43742-1_14
2014 Modelling the semantic web using a type system https://dl.acm.org/citation.cfm?doid=2630602.2630607
2014 Monotonicity reasoning in formal semantics based on modern type theories https://link.springer.com/chapter/10.1007%2F978-3-662-43742-1_11
2014 Natural Language Inference in Coq https://link.springer.com/article/10.1007%2Fs10849-014-9208-x
2014 Small satellite systems design methodology: A formal and agile design process https://ieeexplore.ieee.org/document/6819305/
2014 Specifying well-formed part-whole relations in Coq https://link.springer.com/chapter/10.1007%2F978-3-319-08389-6_14
2014 The montagovian generative lexicon λTyn: A type theoretical framework for natural language semantics http://drops.dagstuhl.de/opus/volltexte/2014/4633/
2014 Typed hilbert epsilon operators and the semantics of determiner phrases https://link.springer.com/chapter/10.1007%2F978-3-662-44121-3_2
2014 TyS - A framework to facilitate the implementation of object-oriented type checkers http://ksiresearchorg.ipage.com/seke/seke14paper/seke14paper_6.pdf
2014 Using signatures in type theory to represent situations https://link.springer.com/chapter/10.1007%2F978-3-662-48119-6_13
2014 Vagueness and learning: A type-theoretic approach https://aclweb.org/anthology/S14-1019
2013 A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation https://link.springer.com/chapter/10.1007%2F978-3-642-38946-7_12
2013 A typed approach for contextualizing the part-whole relation https://link.springer.com/chapter/10.1007%2F978-3-642-40972-1_1
2013 Adjectives in a modern type-theoretical setting https://link.springer.com/chapter/10.1007%2F978-3-642-39998-5_10
2013 Coercive subtyping: Theory and implementation https://www.sciencedirect.com/science/article/pii/S0890540112001757?via%3Dihub
2013 Definitional extension in type theory http://drops.dagstuhl.de/opus/volltexte/2014/4635/
2013 Formal foundations for situation awareness based on dependent type theory https://linkinghub.elsevier.com/retrieve/pii/S1566253512000322
2013 Logical polysemy and subtyping https://link.springer.com/chapter/10.1007%2F978-3-642-39931-2_2
2013 Modelling language, action, and perception in type theory with records https://link.springer.com/chapter/10.1007%2F978-3-642-41578-4_5
2013 Modeling ontological structures with type classes in Coq https://link.springer.com/chapter/10.1007%2F978-3-642-35786-2_11
2013 The montagovian generative lexicon λTyn: A type theoretical framework for natural language semantics http://drops.dagstuhl.de/opus/volltexte/2014/4633/
2012 A Constructive Type-Theoretical Formalism for the Interpretation of Subatomically Sensitive Natural Language Constructions https://link.springer.com/article/10.1007%2Fs11225-012-9431-x
2012 A contextual type theory with judgemental modalities for reasoning from open assumptions https://www.jstor.org/stable/44085222
2012 A modal type theory for formalizing trusted communications https://linkinghub.elsevier.com/retrieve/pii/S1570868311000668
2012 A Type-Theoretical Approach for Ontologies: the Case of Roles https://content.iospress.com/articles/applied-ontology/ao113
2012 An account of natural language coordination in type theory with coercive subtyping https://link.springer.com/chapter/10.1007%2F978-3-642-41578-4_3
2012 Common nouns as types https://link.springer.com/chapter/10.1007%2F978-3-642-31262-5_12
2012 Formal semantics in modern type theories with coercive subtyping https://link.springer.com/article/10.1007%2Fs10988-013-9126-4
2012 Logical polysemy and subtyping https://link.springer.com/chapter/10.1007%2F978-3-642-39931-2_2
2012 Modelling language, action, and perception in type theory with records https://link.springer.com/chapter/10.1007%2F978-3-642-41578-4_5
2012 Type-theoretical dynamics: Exploring belief revision in a constructive framework https://link.springer.com/chapter/10.1007%2F978-94-007-1923-1_11
2012 Type Theory and Semantics in Flux http://lecomte.al.free.fr/ressources/PARIS8_LSL/ddl-final.pdf
2012 Variable types for meaning assembly: A logical syntax for generic noun phrases introduced by most https://journals.openedition.org/rlv/2082
2011 A focused sequent calculus framework for proof-search in pure type systems https://arxiv.org/abs/1012.3372
2011 A single-type logic for natural language https://academic.oup.com/logcom/article/25/4/1111/965440
2011 Contextual analysis of word meanings in type-theoretical semantics https://link.springer.com/chapter/10.1007%2F978-3-642-22221-4_11
2011 Copredication, quantification and frames https://link.springer.com/chapter/10.1007%2F978-3-642-22221-4_5
2011 Using a dependently-typed language for expressing ontologies https://link.springer.com/chapter/10.1007%2F978-3-642-25975-3_23
2011 Using formal methods with SysML in aerospace design and engineering https://link.springer.com/article/10.1007%2Fs10472-011-9267-5
2010 A formal ontology for a computational approach of time and aspect https://link.springer.com/chapter/10.1007%2F978-3-642-14770-8_7
2010 Constructions for modeling product structure http://ceur-ws.org/Vol-614/owled2010_submission_10.pdf
2010 Four semantic layers of common nouns https://link.springer.com/article/10.1007%2Fs11229-009-9533-9
2010 Frames in formal semantics https://link.springer.com/chapter/10.1007%2F978-3-642-14770-8_13
2010 Logic for modeling product structure http://dl.kr.org/dl2010/papers/paper_14.pdf
2010 Modeling Contexts with Dependent Types https://content.iospress.com/articles/fundamenta-informaticae/fi104-4-01
2010 Towards a Type-Theoretical Account of Lexical Semantics https://link.springer.com/article/10.1007%2Fs10849-009-9113-x
2010 Towards Ontological Correctness of Part-whole Relations with Dependent Types http://ebooks.iospress.nl/publication/5591
2010 VeriML: Typed computation of logical terms inside a language with effects https://dl.acm.org/citation.cfm?doid=1863543.1863591
2009 Meta-relation and ontology closure in conceptual structure theory https://link.springer.com/article/10.1007%2Fs10506-009-9082-z
2009 Reasoning about relations with dependent types: Application to context-aware applications https://link.springer.com/chapter/10.1007%2F978-3-642-04125-9_20
2009 Towards an ontological modeling with dependent types: Application to part-whole relations https://link.springer.com/chapter/10.1007%2F978-3-642-04840-1_13
2008 A theorem prover with dependent types for reasoning about actions http://ebooks.iospress.nl/publication/4578
2008 Causal reasoning with contexts using dependent types https://www.aaai.org/Papers/FLAIRS/2008/FLAIRS08-029.pdf
2008 Towards a conceptual structure based on type theory https://pdfs.semanticscholar.org/e485/58aaef2c17cc85f2d969aaa19c6f791d4001.pdf
2008 Type theory with records and unification-based grammar https://pdfs.semanticscholar.org/30bc/0277d55a9a40e52741cafe83d32570f793f9.pdf
2007 An epistemic constructive definition of information https://www.jstor.org/stable/44084876
2007 Dependent record types for dynamic context representation https://doi.org/10.1007/978-1-84628-663-6-15
2007 Goal reasoning with context record types https://link.springer.com/chapter/10.1007%2F978-3-540-74255-5_13
2007 Interpreting metaphors in a new semantic theory of concept https://link.springer.com/chapter/10.1007%2F978-3-540-69902-6_16
2007 On the representation of imperative programs in a logical framework https://link.springer.com/chapter/10.1007%2F978-3-540-75867-9_26
2007 Using contexts to prove and share situations https://pdfs.semanticscholar.org/37eb/7936ad526ff076dcf2bfb93f49fad904db96.pdf
2006 A sequent calculus for type theory https://link.springer.com/chapter/10.1007%2F11874683_29
2005 Abstraction and ontology: Questions as propositional abstracts in type theory with records https://academic.oup.com/logcom/article-abstract/15/2/113/1079197?redirectedFrom=fulltext
2005 Austinian truth, attitudes and type theory https://link.springer.com/article/10.1007%2Fs11168-006-0002-z
2005 Records and record types in semantic theory https://academic.oup.com/logcom/article/15/2/99/1079193
2005 Situation semantics: The ontological balance sheet https://link.springer.com/article/10.1007%2Fs11168-006-6329-7
2004 Ontological feedback in multiagent systems https://ieeexplore.ieee.org/document/1373469?section=abstract
2004 Types for Web Rule Languages: a preliminary study. Technical report A04-R-560 https://hal.inria.fr/inria-00099859/document
2003 A constructive approach to state description semantics https://www.sciencedirect.com/science/article/pii/S157086830300003X?via%3Dihub
2003 Constructive semantics for extensional PTQ https://ieeexplore.ieee.org/document/1232871
2000 Formalizing Context in Intuitionistic Type Theory https://content.iospress.com/articles/fundamenta-informaticae/fi42-2-01
1996 Type theoretic semantics for semnet https://link.springer.com/chapter/10.1007%2F3-540-61313-7_102
1995 Towards high-level deductive program synthesis based on type theory https://ieeexplore.ieee.org/document/490133
1992 An implementation of the entity-relationship model in type theory https://ieeexplore.ieee.org/document/271931
1991 Formal representation of semantic data models in type theory https://ieeexplore.ieee.org/document/729670

UPDATE: обсуждение в чатике по типам -- https://t.me/typeslife/4853
post comment

lytdybr [24 Sep 2019|02:50pm]
Через пару часов на сутки вылетаю в Казань, буду рассказывать участникам очного этапа республиканского конкурса "Инженер года" (http://mpt.tatarstan.ru/rus/respublikanskiy-konkurs-inzhener-goda.htm) про всякое и разное мышление.

А в четверг уже буду учиться работать с MS Teams, целый день (это я потихоньку двигаюсь в сторону реализации blended learning на базе идёй текста про PLM+CAD для образования -- https://ailev.livejournal.com/1473691.html).

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

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

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

navigation
[ viewing | September 24th, 2019 ]
[ go | previous day|next day ]