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