|
Lundi 19 Janvier
| Heure: |
13:30 - 15:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
A Text Analytic Approach to Historical Legal Records |
| Description: |
Adam Zachary Wyner The council registers of Aberdeen, Scotland are the earliest and most complete body of town (or burgh) council records in Scotland, running nearly continuously from 1398 to the present; they are hand written in Latin and (largely) Middle Scots. Few cities in the United Kingdom or in Western Europe rival Aberdeen's burgh registers in historical depth and completeness. In July 2013, UNESCO UK recognised the register volumes from 1398 to 1509 as being of outstanding historical importance to the UK. The registers offer a detailed view into the legal aspects of life in one of Scotland's principal burghs, providing a view into administrative, legal, and commercial activities as well as daily life. The registers include information about a range of matters, from the elections of office bearers, property transfers, regulations of trade and prices, references to crimes and subsequent punishment, to matters of public health, credit and debt, cargoes of foreign vessels, tax and rental o
f burgh lands, and woods and fishings. Thus the entries present the burgh's relationships with the countryside and countries around the North Sea.
This talk discusses the results of a text analytic project developed around 100 transcribed pages of these records from the period 1530-1531. We worked with the General Architecture for Text Engineering (GATE) text analytic tool. In the project, we created a large, rich, and varied range of semantic annotations such as individual's names, locations, various materials of trade, legal concepts, translation, offices, social status, documents, shipping terminology, and many others. The annotations can be examined either in situ or as complex semantic queries.
With this application, users can hover over the text and receive a translation into English, making the text accessible to a large audience. Legal historians can query and study the text in novel and illuminating ways, for example, rapidly examining the use of particular terminology or patterns over the whole corpus. Moreover, legal historians can scale up their textual studies - while the particular tool was developed for only 100 pages, it can be applied to larger corpus of related material of some 600 pages. The tool is also highly extensible, allowing for modification of the current analysis as well as the addition of other material that may be beyond the scope of the Aberdeen registers.
We outline the project objectives, present the text analytic tool, show the range of annotations, provide some sample results of queries, relate our work to other projects, and sketch future work. Broadly, the paper and project contribute to the application of language technologies for cultural heritage and the humanities. More specifically, the research provides a text analytic approach to studying the evolution of legal concepts and their application over time, providing legal historians with the means to gain fresh insights to historical and contemporary legal systems. |
Mardi 20 Janvier
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Statistical physics and combinatorics |
| Description: |
Francesco Caltagirone |
Mercredi 21 Janvier
| Heure: |
14:00 - 15:00 |
| Lieu: |
Amphi A |
| Résumé: |
Quantum Computing: From physics to computational systems |
| Description: |
Andrea Masini |
Jeudi 22 Janvier
| Heure: |
16:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Specification and verification of Time Petri Nets with Coq |
| Description: |
Amal Chamakh Model checking and theorem proving, have long reached their limitation as
general-purpose techniques, and most of the research now is concentrated on
efficient specialization of both approaches to relatively narrow problem
domains. The state space explosion problem leaves little hope for automatic
finite-state verification techniques like model checking to remain
practical, especially when designs become parameterized. The use of theorem
proving techniques is inevitable to cope with the new verification
challenges. "Pure" theorem proving, on the other hand, can also be quite
tedious and impractical for complex designs. Ideally, one would like to
find an efficient combination of model checking and theorem proving, and
the quest for such a combination has long been one of the major challenges
in the field of formal verification. In this paper, we address the
combination of model checking and theorem proving approaches in order to
specify and to model check Time Petri Nets (TPN) model-based systems. In
particular, we show how a TPN is specified using the Coq proof assistant,
and how the fireability/unfireability of a timed sequence of transitions
can be proved. This allows, for instance, to prove the reachability of a
given state by the firing of a given timed/untimed trace or to prove that a
counter-example supplied by a given (untimed) model checker is a real
counterexample of a timed system. %First, we provide a formalization of the
net model in COQ via the parsing of its Petri Net Markup Language (PNML)
description. Then the COQ proof assistant is used to prove the firability
(or the opposite) of traces given by model checking as a counter-example
when a propriety being checked is found to be non-valid, hence, states
reachability is proved. |
Vendredi 23 Janvier
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
An Introduction to Higher-Dimensional Rewriting Theory |
| Description: |
Samuel Mimram À venir. |
|
|
