forked from pirofti/los.cs.unibuc.ro
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathseminar-logic.html
329 lines (285 loc) · 12.2 KB
/
seminar-logic.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
<!DOCTYPE HTML>
<!--
Theory by TEMPLATED
templated.co @templatedco
Released for free under the Creative Commons Attribution 3.0 license (templated.co/license)
-->
<html>
<head>
<title>Research Center for Logic, Optimization and Security (LOS)</title>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<link rel="stylesheet" href="assets/css/main.css" />
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
inlineMath: [ ['$','$'], ["\\(","\\)"] ],
processEscapes: true
}
});
</script>
<script type="text/javascript"
src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
</script>
</head>
<body>
<!-- Header -->
<header id="header">
<div class="inner">
<span class="circle">
<b> LOS </b>
</span>
<nav id="nav">
<a href="news.html"> NEWS</a>
<a href="index.html#about"> ABOUT</a>
<a href="index.html#people"> PEOPLE</a>
<a href="index.html#projects">PROJECTS</a>
<a href="index.html#seminars">SEMINARS</a>
<a href="index.html#publications">PUBLICATIONS</a>
</nav>
<a href="#navPanel" class="navPanelToggle"><span class="fa fa-bars"></span></a>
</div>
</header>
<!-- Banner -->
<section id="banner">
<h1>Logic Seminar</h1>
<p>Logic, Optimization & Security</p>
<p>DEPARTMENT of COMPUTER SCIENCE</p>
<p>FACULTY of MATHEMATICS and COMPUTER SCIENCE</p>
<p> UNIVERSITY of BUCHAREST </p>
</section>
<section id="logic-seminar" class="wrapper special">
<div class="inner">
<header style="text-align:left;">
<h3>The logic seminar is a joint LOS-<a href="http://imar.ro">IMAR</a> seminar. <br>
Organizers:
<a href="https://cs.unibuc.ro/~lleustean">Laurențiu Leuștean</a> and
<a href="https://cs.unibuc.ro/~asipos/">Andrei Sipoș</a></h3>
</header>
<div class="flex flex-3">
<article>
<p>The logic seminar features talks on mathematical logic, philosophical logic and logical aspects of computer science.</p>
</article>
<article>
<p>All seminars, except where otherwise indicated, will be Thursdays between 10:00 and 11.50.
The seminars are online.
<!--hybrid, both remotely and in the Google Hall of the
<a href="https://fmi.unibuc.ro">Faculty of Mathematics and Computer Science</a>,
University of Bucharest.--></p>
</article>
<article>
<p>To receive announcements about the seminar, please send an email to
<a href="mailto:logic_seminar@fmi.unibuc.ro">logic_seminar@fmi.unibuc.ro</a>.</p>
</article>
</div>
</div>
</section>
<section id="about" class="wrapper special">
<div class="inner">
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, October 21, 2021</h3>
</header>
<p style="text-align:left;">
Mihai Prunescu (University of Bucharest and IMAR)
<br>
On Representations of Intended Structures in Foundational Theories
<br><br>
Abstract: Often philosophers, logicians, and mathematicians employ a notion of intended
structure when talking about a branch of mathematics. In addition, we know that there are
foundational mathematical theories that can find representatives for the objects of informal
mathematics. In this paper, we examine how faithfully foundational theories can represent
intended structures, and show that this question is closely linked to the decidability of
the theory of the intended structure. Joint work with Neil Barton and Moritz Muller.
<br>
References: <br>
[1] N. Barton, M. Müller, M. Prunescu, <a href="https://link.springer.com/article/10.1007%2Fs10992-021-09628-2">
On Representations of Intended Structures in Foundational Theories</a>.
Journal of Philosophical Logic (2021).<br>
<a href="https://doi.org/10.1007/s10992-021-09628-2">DOI: 10.1007/s10992-021-09628-2</a>
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, October 28, 2021</h3>
</header>
<p style="text-align:left;">
<a href="https://cs.unibuc.ro/~bmacovei/">Bogdan Macovei</a> (LOS)
<br>DELP: Dynamic Epistemic Logic for Security Protocols
<br><br>
Abstract: The formal analysis of security protocols is a challenging field, with various approaches
being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to
validate security protocols. Combining ideas from previous approaches, in this paper we define a complete
system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of
its properties are verifyied, using the theorem prover Lean.
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, November 11, 2021</h3>
</header>
<p style="text-align:left;">
<a href="https://scholar.google.co.uk/citations?user=10v2GlMAAAAJ&hl=en">Ionuţ Ţuţu</a> (IMAR)
<br>
A Rewriting-based Toolset for Specification Processing
<br><br>
Abstract: We explore some of the features that promote term rewriting
and, in particular, Maude as a meta-language for working with logical
systems, and showcase a set of rewriting-based tools that support the
syntactic analysis and processing of formal specifications. Along the
way, we discuss basic aspects related to the development of
interpreters of specification languages, including user-interface
design, parsing specifications, and executing commands. All this is
done in a logic-agnostic manner, meaning that the techniques we
describe apply to a wide variety of logical formalisms. To illustrate
the approach, we introduce SpeX, a general platform for working with
formal specifications, and demonstrate the steps required for
integrating new logical formalisms within SpeX.
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, November 18, 2021, 10:30</h3>
</header>
<p style="text-align:left;">
<a href="https://www.andreipopescu.uk">Andrei Popescu</a> (University of Sheffield)
<br>
Inductive and Coinductive Reasoning with Isabelle/HOL
<br><br>
Abstract: I will describe basic and advanced mechanisms for inductive
and coinductive reasoning available in the interactive theorem prover
Isabelle/HOL. They cover inductive and coinductive predicates founded
on Knaster-Tarski fixed points, inductive and coinductive datatypes,
structural recursion and corecursion, corecursion "up-to" and mixed
recursion-corecursion. The concepts will be illustrated with examples
formalized in Isabelle, but they should be understandable to computer
scientists, logicians and mathematicians with no knowledge of
Isabelle.
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, November 25, 2021</h3>
</header>
<p style="text-align:left;">
<a href="https://cs.unibuc.ro/~tserbanuta/">Traian Şerbănuţă</a> (LOS & Runtime Verification)
<br>
Consensus in Distributed Systems. Formalizing Correct by Construction Protocols
<br><br>
Abstract: This presentation will attempt to review the basic definitions andresults concerning
the consensus problem for distributed protocols (byzantine faults, safety, liveness), discuss
Vlad Zamfir's idea of correct-by-construction protocols and our attempts at formalizing his approach.
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, December 2, 2021</h3>
</header>
<p style="text-align:left;">
<a href="https://rdiaconescu.weebly.com">Răzvan Diaconescu</a> (IMAR)
<br>
Experimental Mathematics by Rewriting
<br><br>
Abstract: This talk is about how to support mathematical investigation and development through machine
performed computational experiments. Its unique character lies in a computational method and its
associated programming technique.
This is based an extended form of model-theoretic rewriting which includes some powerful
features such as non-determinism and rule-based programming. It is also universal in the sense
that that it is applicable in principle to a wide variety of mathematical domains. Its solid and
transparent mathematical and logical foundations lead to a programming experience that is very
close to doing mathematics, which means it is much more suitable for mathematicians than other
forms of do-it-yourself programming. The talk will touch directly two aspects of this
activity: model-theoretic foundations and case studies.
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, December 9, 2021</h3>
</header>
<p style="text-align:left;">
<a href="https://cs.unibuc.ro/~asipos/">Andrei Sipoş</a> (LOS and IMAR)
<br>
On extracting variable Herbrand disjunctions
<br><br>
Abstract: Some quantitative results obtained by proof mining take the form of Herbrand disjunctions
that may depend on additional parameters. We attempt to elucidate this fact through an extension
to first-order arithmetic of the proof of Herbrand's theorem due to Gerhardy and Kohlenbach which
uses the functional interpretation. <br>
References: <br>
[1] A. Sipoş, <a href="https://arxiv.org/abs/2111.12133">
On extracting variable Herbrand disjunctions</a>,
arXiv:2111.12133 [math.LO] (2021).
</p>
</article>
<article>
<header style="text-align:left;">
<h3 id="content">Thursday, December 16, 2021</h3>
</header>
<p style="text-align:left;">
Bogdan Dumitru (University of Bucharest)
<br>SAT Solvers: Introduction and applications
<br><br>
Abstract: SAT solving theory and practice made dramatic progress in the last decade, to the point
where problems with millions of variables and clauses can be solved in a timely manner.
We explore the ingredients of modern SAT solvers and study some of their applications.
</p>
</article>
<!--<article>
<header style="text-align:left;">
<h3 id="content">Thursday, December 2, 2021</h3>
</header>
<p style="text-align:left;">
Mircea Dumitru (University of Bucharest)
<br>
Modalities and Quantifiers. Possible Worlds or Counterparts?
<br><br>
Abstract: TBA
</p>
</article>
-->
</div>
</section>
<section id="past seminars" class="wrapper">
<div class="inner"><header class="align-left"><h3>Past seminars</h3></header>
<ul>
<li> <a href="Logic seminar - past/seminar-logic-2020-2021.html">LOS/IMAR Logic Seminar in 2020-2021</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2019-2020.html">FMI/IMAR Logic Seminar in 2019-2020</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2018-2019.html">FMI/IMAR Logic Seminar in 2018-2019</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2017-2018.html">FMI/IMAR Logic Seminar in 2017-2018</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2016-2017.html">FMI/IMAR Logic Seminar in 2016-2017</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2015-2016.html">FMI/IMAR Logic Seminar in 2015-2016</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2014-2015.html">FMI/IMAR Logic Seminar in 2014-2015</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2013-2014.html">IMAR Logic Seminar in 2013-2014</a> </li>
<li> <a href="Logic seminar - past/seminar-logic-2012-2013.html">IMAR Logic Seminar in 2012-2013</a> </li>
<li> <a href="https://sites.google.com/site/locsseminar/">FMI Logic in Computer Science Seminar in 2014</a></li>
<li> <a href="https://sites.google.com/site/locsseminar/locs2013">FMI Logic in Computer Science Seminar in 2013</a></li>
</ul>
</h3>
</div>
</section>
<!-- Footer -->
<footer id="footer" style="background-color:white;">
<div class="inner">
<div class="flex">
<div class="copyright">
© Untitled. Design: <a
href="https://templated.co">TEMPLATED</a>
(<a href="https://creativecommons.org/licenses/by/3.0/legalcode">CC BY 3.0</a>).</a>.
</div>
<!-- <ul class="icons">
<li><a href="#" class="icon fa-facebook"><span class="label">Facebook</span></a></li>
<li><a href="#" class="icon fa-twitter"><span class="label">Twitter</span></a></li>
<li><a href="#" class="icon fa-linkedin"><span class="label">linkedIn</span></a></li>
<li><a href="#" class="icon fa-pinterest-p"><span class="label">Pinterest</span></a></li>
<li><a href="#" class="icon fa-vimeo"><span class="label">Vimeo</span></a></li>
</ul> -->
</div>
</div>
</footer>
<!-- Scripts -->
<script src="assets/js/jquery.min.js"></script>
<script src="assets/js/skel.min.js"></script>
<script src="assets/js/util.js"></script>
<script src="assets/js/main.js"></script>
</body>
</html>