11月7日：Jean-Marie Madiot：A formal proof that well synchronized C programs run correctly on weakly consistent machines

报告题目：A formal proof that well synchronized C programs run correctly on weakly consistent machines

报告人：Daniel Hirschkoff 教授、POUS, Damien教授

主持人：王长波

报告时间：11月7日 13:00-15:00

报告地点：中北校区数学馆201

报告摘要：

We prove that concurrent C programs, proved correct using separation logic, obey their specification after compilation and run on weakly consistent machines such as x86-TSO. We use two fundamental principles: 1) well synchronized programs should not have data races,and 2) programs whose sequentially consistent executions have no data races should run on weakly consistent multiprocessors as if they were sequentially consistent. The former claim comes from Dijkstra and Hoare through formalizations by O'Hearn and Brookes; the latter was stated by Saraswat et al. as a desideratum for compilers and multiprocessors.

We prove these claims for concurrent separation Logic, the CompCert C compiler, and the Intel x86 (IA-32) computer architecture.  C programs provable in concurrent separation logic, when compiled with this optimizing C compiler and run on that machine, will have the (sequentially consistent) behavior proved at the source level. Our proof is modular: a theorem about the soundness of CSL with respect to the operational semantics of C (and our 5 synchronization functions);a theorem about the correctness of the C compiler; a theorem about the Intel x86-TSO architecture.

11月7日：GQ Zhang：The role of ontologies in clinical and translational informatics

报告题目: The role of ontologies in clinical and translational informatics

报告人：Prof. GQ Zhang, University of Kentucky

主持人：陈仪香

报告时间：11月7日15:30--16:30

报告地点：数学馆201会议室

报告摘要：

This talk will present the role of ontologies in clinical and translational informatics, illustrated using specific research data resource examples.One such resource is the National Research Resource grant (R24HL114473), to establish the NHLBI National Sleep Research Resource, a comprehensive, easily accessible and well-annotated national repository of sleep data to make data from more than 50,000 sleep studies available to biomedical researchers.The second is the MEDCIS Data Repository for the NINDS-funded Center for SUDEP Research (U01NS090408), a prospective collaborative involving 14 institutions for the understanding of sudden unexpected death in epilepsy. The use of a Sleep Domain Ontology and Epilepsy and Seizure Ontology in both resources are discussed. In the second part of the talk, recent developments in non-lattice auditing of biomedical ontologies such as SNOMED CT and GO are presented.

报告人简介：

GQ Zhang, PhD，Institute of Biomedical Informatics, University of Kentucky，Dr. Zhang is Professor of Internal Medicine and Computer Science at the University of Kentucky, where he is the Director of the Institute of Biomedical Informatics;  Chief of the Division of Biomedical Informatics(https://bmi.med.uky.edu); Associate Director, Center for Clinical & Translational Science (http://www.ccts.uky.edu/ccts/BMI_Core); and Director, Informatics & Data Analytics Core, NINDS-CWW Center for SUDEP Research (sudepresearch.org).Prior to joining the University of Kentucky, his role at Case Western Reserve University included Division Chief of Medical Informatics,Co-Director of Biomedical Research Information Management Core of the Case Western CTSA,and Associate Director for Case Comprehensive Cancer Center while performing duties as a tenured professor in the Case School of Engineering.

His research interests include data science and bigdata in biomedicine, large-scale, multi-center data integration,biomedical ontology development, information retrieval, query interface design, and agile, interface-driven,access-control grounded software development. These interests are reflected in his over 130 publications in

Computer Science and Biomedical Informatics. Over more than a decade, Dr. Zhang has developed a range of clinical research informatics toolsfor data capturing, data management, cohort discovery, and clinical decision support, such as VISAGE (PMID: 21347154),MEDCIS (PMID: 23686934), OnWARD (PMID: 21924379), OPIC (PMID: 23304354), EpiDEA (PMID: 23304396), and Cloudwave (PMID: 23920671).

Supported by multiple federal- and foundation-funded awards and acclimated in a multi-disciplinary team-science, collaborative setting,Dr. Zhang effectively brings cutting-edge computer science and informatics methodology to addressing biomedical data/big data challengesthrough the translation of theory, algorithms, methods and best practices to functional and usable tools impacting the entire clinical research data lifecycle.

             11月8日：Pierre-Louis Curien：Hypergraph polytopes and weak Cat-operads, after Dosen and Petric

报告题目：Hypergraph polytopes and weak Cat-operads, after Dosen and Petric
报告人：Pierre-Louis Curien （法国巴黎第七大学教授）
主持人：邓玉欣
时间：11月8日 13:00-15:00
地点：中北校区数学馆201
报告摘要：
Dosen and Petric, following earlier work of Devadoss and others, have used hypergraphs to describe a class of polytopes lying between the permutohedron and the simplex, obtained by successive truncations of faces of the latter (at all dimensions)   The key notion is that of constructs (for which we provide an efficient notation),  which are combinatorial structures derived from the structure of the hypergraph under study and serve for naming  all the faces of an abstract  polytope.Just like associahedra arise in the coherence of monoidal categories,  several polytopes (the associahedron, the permutohedron, and a third one, called hemi-associahedron) intervene in the investigation of the notion of weak Cat-operad (aslo due to Dosen and Petric), which I shall introduce.Coherence is in turned linked to rewrting theory!  I'll motivate the whole talk by recalling the famous Mac Lane pentagone (a two-dimensional polytope)  arising from the critical pair formed by the associativity rule and itself.  Critical triples give rise to three-dimensional polytopes.

11月9日：何积丰：Modeling Probabilistic Programming

讲座题目：Modeling Probabilistic Programming
报告人： 何积丰  院士/教授

主持人：李钦
开始时间：2016年11月9日  13:30—15:00

报告地点：中北校区理科大楼B1002
报告摘要：
Formal methods advocate the crutial role played by the algebraic approach in specification and implementation of programs. Traditionally, a top-down approach (with denotational model as its origin)links the algebra of programs with the denotational representation by establishment of the soundness and completeness of the algebra against the given model, while a bottom-up approach (a journey started from operational model) introduces a variety of bisimulations to establish the equivalence relation among programs. This paper adopts a new approach presented in “A New Roadmap of Linking Theories of Programming” to deal with probabilistic programming, by construction of an algebra of probabilistic programs as its origin, and then derivation of both denotational model and transition system.

11月10日：汤庸：学术社交网络及大数据研究与实践

报告题目：学术社交网络及大数据研究与实践
报告人：汤庸 教授

主持人：林学民

报告时间：2016年11月10日 10:00

报告地点：中北校区数学馆201室

报告摘要：

本报告以我们自主开发学术社交网络SCHOLAT（学者网）为背景，介绍个人学术空间数据管理，面向学者的学术圈创建及通讯，基于SCHOLAT的科研教学协作，SCHOLAT学术搜索和学术门户等。最后讨论基于SCHOLAT大数据的信息服务接口及应用示例。

报告人简介：

汤庸学者网创始人，华南师范大学学位委员会副主席、计算机学院院长，二级教授、博士导师，获武汉大学学士和硕士学位、中国科学技术大学博士学位。享受国务院政府特殊津贴，首批教育部新世纪优秀人才入选者，中国计算机学会首批杰出会员，获宝钢教育奖、丁颖科技奖、南粤教坛新秀、中山大学教学名师，以第一完成人获广东省科学技术奖一等奖、教育部提名国家科学技术奖二等奖、广东省优秀学术论文一等奖及省教学成果一等奖等。