seminar-Lean-temp.html

<section class="special lean">
	<div class="inner">
		<header>
		<h2>RESEARCH PROJECTS IN LEAN</h2>
		</header>
	</div>
</section>


<section class="lean-projects">
<div class="slideshow-container">

  <div class="description">
  	<h3 class="title">Formalized Mathematics</h3>
    <q>Formalized mathematics is a subject that gained traction in recent years, 
    and Lean is the host of one of the largest and most active projects in the field,
    through its de facto standard library, mathlib [1].
    Nevertheless, fundamental mathematical notions and results are still missing, some examples
    can be seen in [2].</q>
    <br>
    <br>
    <q>
    References:
    <br>
    [1]  The mathlib Community. <a href="https://leanprover-community.github.io/papers/mathlib-paper.pdf">
    The Lean mathematical library</a>. In J.  Blanchette and C. Hrițcu, 
    editors, <i>Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs 
    and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020</i>, pages 367–381. ACM, 2020.
    <br>
    [2] <a href="https://leanprover-community.github.io/undergrad_todo.html">The Lean
    Prover Community</a>
    </q>
  </div>

  <div class="description">
  	<h3 class="title">Program extraction by proof mining</h3>
    <q> Proof mining [3] is a research field in applied mathematical logic 
      which has the goal of extracting, from mathematical proofs, quantitative informations 
      (algorithms, computable bouns) or 
      qualitative (the weakening of the premises, the uniformity of the bounds).
      Proof-theoretical results and techniques, in the form of general logical 
      metatheorems, offer rigorous guarantees that such 
      information may be extracted. Furthermore, due to the constructive character 
      of their proofs, the metatheorems also provide algorithms for extracting bounds 
      and proofs of the correctness of the extracted bounds.
      By implementing in Lean the logical systems from proof mining and the proofs of 
      the metatheorems, 
      we wish to construct a system for automatic bound extraction from mathematical proofs 
      by proof mining methods.
    </q>
    <br>
    <br>
    <q>
    References:
    <br>
    [1] P. Gerhardy and U. Kohlenbach. General logical metatheorems for functional analysis. 
    <i>Transactions of the American Mathematical Society</i>, 360(5):2615–2660, 2008.
    <br>
    </q>
  </div>

  <div class="description">
    <h3 class="title">Matching Logic implementation in Lean</h3>
    <q>Matching logic is a unifying foundational logic for programming languages, 
      specification, verification. It serves as the foundation of the K framework [1]: 
      a formal language framework where different programming languages  have a formal 
      semantics and different language tools are automatically generated by the framework 
      from the semantics at no additional costs, in a correct-by-construction manner [2].
    </q>
    <br><br>
    <q>
      References:
      <br>
      [1] <a href="https://kframework.org/">K framework</a>
      <br>
      [2] <a href="http://www.matching-logic.org/">Matching Logic</a>
    </q>
  </div>

  <div class="description">
  	<h3 class="title">Formal Verification of Security Protocols</h3>
    <q>The formal analysis of security protocols is a challenging field, 
      with various approaches being studied nowadays. The famous Burrows-Abadi-Needham (BAN) Logic [1] 
      was the first logical system aiming to validate security protocols. 
      Combining ideas from previous approaches [3, 4], a complete system 
      of Dynamic Epistemic Logic (DELP) for modeling security protocols, was defined in [2]. This logic is implemented,
      and a few of its properties are verified using the theorem prover Lean.
    </q>
    <br>
    <br>
    <q>
      References:
      <br>
      [1] Burrows, Michael, Martin Abadi, and Roger Michael Needham. 
      "A logic of authentication." 
      <i>Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences</i>
      426.1871 (1989): 233-271.
      <br>
      [2] Leuștean, Ioana and Macovei, Bogdan. DELP: 
      Dynamic Epistemic Logic for Security Protocols, 2021; arXiv:2109.05599.
      <br>
      [3] Halpern, Joseph Y., Ron van der Meyden, and Riccardo Pucella. 
      "An epistemic foundation for authentication logics." 
      <i>arXiv preprint arXiv:1707.08750</i> (2017).
      <br>
      [4] Van Ditmarsch, Hans, et al. 
      "Hidden protocols: Modifying our expectations in an evolving world." 
      <i>Artificial Intelligence</i> 208 (2014): 18-40.
    </q>
    </div>

  <a class="prev" onclick="plusSlides(-1)">&#10094;</a>
  <a class="next" onclick="plusSlides(1)">&#10095;</a>
</div>
</section>	
	

<style>
.slideshow-container {
  position: relative;
  background: white;
}

.description {
  display: none;
  padding-top: 30px;
  padding-right: 80px;
  padding-left: 100px;
  padding-bottom: 100px;
}

.prev, .next {
  cursor: pointer;
  position: absolute;
  top: 50%;
  width: auto;
  margin-top: -30px;
  padding: 16px;
  color: #888;
  font-weight: bold;
  font-size: 20px;
  border-radius: 0 3px 3px 0;
  user-select: none;
}

.next {
  position: absolute;
  right: 0;
  border-radius: 3px 0 0 3px;
}

.prev:hover, .next:hover {
  background-color: rgba(0,0,0,0.8);
  color: white;
}

.dot-container {
  text-align: center;
  padding: 20px;
  background: #ddd;
}

.dot {
  cursor: pointer;
  height: 15px;
  width: 15px;
  margin: 0 2px;
  background-color: #bbb;
  border-radius: 50%;
  display: inline-block;
  transition: background-color 0.6s ease;
}

.active, .dot:hover {
  background-color: #717171;
}

q {
	font-size: 16px;
	text-align: left;
}

.title {
	text-align: center;
}

.lean {
	font-size: 24px;
	margin-bottom: 0px;
}
</style>

<script>
var slideIndex = 1;
showSlides(slideIndex);

function plusSlides(n) {
  showSlides(slideIndex += n);
}

function currentSlide(n) {
  showSlides(slideIndex = n);
}

function showSlides(n) {
  var i;
  var slides = document.getElementsByClassName("description");
  var dots = document.getElementsByClassName("dot");
  if (n > slides.length) {slideIndex = 1} 
    if (n < 1) {slideIndex = slides.length}
    for (i = 0; i < slides.length; i++) {
      slides[i].style.display = "none"; 
    }
    for (i = 0; i < dots.length; i++) {
      dots[i].className = dots[i].className.replace(" active", "");
    }
  slides[slideIndex-1].style.display = "block"; 
  dots[slideIndex-1].className += " active";
}

</script>