update titles/abstracts

Author: zliu41

uplc2025/_data/program.yml

@@ -35,7 +35,7 @@ days:
         - name: 'Aiken Type System: Past, Present, Future'
           time_start: '15:50'
           time_end: '16:50'
-        - name: TBD-Firth
+        - name: Hydra Plutus/Aiken Review
           time_start: '17:00'
           time_end: '17:20'
 
@@ -69,7 +69,7 @@ days:
         - name: UPLC Costing
           time_start: '14:50'
           time_end: '15:30'
-        - name: TBD-Tudor
+        - name: 'Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano'
           time_start: '15:40'
           time_end: '16:20'
         - name: TBD-Wu

uplc2025/_talks/firth.md

@@ -1,5 +1,5 @@
 ---
-name: TBD-Firth
+name: Hydra Plutus/Aiken Review
 speakers:
   - Daniel Firth
 categories:

uplc2025/_talks/jacco.md

@@ -5,3 +5,8 @@ speakers:
 categories:
   - Talk
 ---
+The formal verification of an optimising compiler for a realistic programming language is no small task. Most verification efforts develop the compiler and its correctness proof hand in hand.
+Unfortunately, this approach is less suitable for today’s constantly evolving community-developed open-source compilers and languages.
+I will discuss an alternative approach to high-assurance compilers, where a separate certifier uses translation validation to assess and certify the correctness of each individual compiler run.
+I will also demonstrate that an incremental, layered architecture for the certifier improves assurance step-by-step and may be developed largely independently from the constantly changing main compiler code base.
+This approach to compiler correctness is practical, as witnessed by the development of a certifier for the PIR-to-PIR pipeline of the Plinth compiler in the Rocq prover.

uplc2025/_talks/nuzzi.md

@@ -5,3 +5,4 @@ speakers:
 categories:
   - Talk
 ---
+Michele will go through the geological strata of Pebble’s history from the initial idea, the plu-ts implementation, the complete rework for Pebble and the future.

uplc2025/_talks/tudor.md

@@ -1,5 +1,5 @@
 ---
-name: TBD-Tudor
+name: 'Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano'
 speakers:
   - Tudor Ferariu
 categories: