This is a bit of a late announcement, but I successfully defended my PhD thesis!
It is about the exploration of a new paradigm for building formal proofs interactively that I call "Proof-by-Action", where the textual tactics of state-of-the-art proof assistants are replaced by direct manipulation actions on the proof state in a GUI. This is founded on a recent branch of structural proof theory called "deep inference".
The manuscript is now officially available on HAL: https://theses.hal.science/tel-04698985.
Pablo Donato /
npub1y7…xz8vm
2024-09-20 09:34:03
Author Public Key
npub1y7w5atu07wz04hjnc25ehlsjzyxrj9zjj3m4429fl2eddqj7na9s7xz8vmSeen on
wss://relay.mostr.pubPublished at
2024-09-20 09:34:03Event JSON
{
"id": "4cb2ff776b89a63f330f78b8607d357a9694c85320a822ab48c6f14db90c57b5",
"pubkey": "279d4eaf8ff384fade53c2a99bfe12110c39145294775aa8a9fab2d6825e9f4b",
"created_at": 1726824843,
"kind": 1,
"tags": [
[
"proxy",
"https://social.sciences.re/users/pablogician/statuses/113169192928980223",
"activitypub"
]
],
"content": "This is a bit of a late announcement, but I successfully defended my PhD thesis!\n\nIt is about the exploration of a new paradigm for building formal proofs interactively that I call \"Proof-by-Action\", where the textual tactics of state-of-the-art proof assistants are replaced by direct manipulation actions on the proof state in a GUI. This is founded on a recent branch of structural proof theory called \"deep inference\".\n\nThe manuscript is now officially available on HAL: https://theses.hal.science/tel-04698985.",
"sig": "9dff5ecf6090dbc45bc396733bca0f7620c5769a2a4429fdd89da73a2b010165233fed8e5501fe89f1b720d83e456f7fe74d9bb3a5c99b40dbae343de31d2650"
}