José A. Alonso on Nostr: Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre ...
Published at
2025-01-11 07:41:18Event JSON
{
"id": "848d29b75bbd298ddbdb5b69f689b2e6ce85cc9d23add9d88d97801acaaff9f5",
"pubkey": "0efb7bc903f4c6716cd4d07830d344d7abe5b607a156de3cde1ac1a5bf22ae1c",
"created_at": 1736581278,
"kind": 1,
"tags": [
[
"t",
"rocq"
],
[
"t",
"coq"
],
[
"t",
"itp"
],
[
"proxy",
"https://mathstodon.xyz/users/Jose_A_Alonso/statuses/113808590675831528",
"activitypub"
]
],
"content": "Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre Corbineau, Basile Gros, Jean-François Monin. https://hal.science/hal-04859450v1/file/jfla2025-final36.pdf #ITP #Coq #Rocq",
"sig": "3d1e9c48dae9c20c2513f7879ac89b10ebe696347277852a1e2bd6ae40472860dda36dd1274685d20104dc0747105c8f8f102988ec20791d7539d411d7a76129"
}
