A Curry-Howard approach to church's synthesis
Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata a...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Schloss Dagstuhl
2017
|
| _version_ | 1826305038018936832 |
|---|---|
| author | Pradic, P Riba, C |
| author_facet | Pradic, P Riba, C |
| author_sort | Pradic, P |
| collection | OXFORD |
| description | Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model. |
| first_indexed | 2024-03-07T06:26:47Z |
| format | Conference item |
| id | oxford-uuid:f4934a4c-ecd2-4a51-b5d4-9d0cf34ff681 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:26:47Z |
| publishDate | 2017 |
| publisher | Schloss Dagstuhl |
| record_format | dspace |
| spelling | oxford-uuid:f4934a4c-ecd2-4a51-b5d4-9d0cf34ff6812022-03-27T12:20:48ZA Curry-Howard approach to church's synthesisConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f4934a4c-ecd2-4a51-b5d4-9d0cf34ff681Symplectic Elements at OxfordSchloss Dagstuhl2017Pradic, PRiba, CChurch's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model. |
| spellingShingle | Pradic, P Riba, C A Curry-Howard approach to church's synthesis |
| title | A Curry-Howard approach to church's synthesis |
| title_full | A Curry-Howard approach to church's synthesis |
| title_fullStr | A Curry-Howard approach to church's synthesis |
| title_full_unstemmed | A Curry-Howard approach to church's synthesis |
| title_short | A Curry-Howard approach to church's synthesis |
| title_sort | curry howard approach to church s synthesis |
| work_keys_str_mv | AT pradicp acurryhowardapproachtochurchssynthesis AT ribac acurryhowardapproachtochurchssynthesis AT pradicp curryhowardapproachtochurchssynthesis AT ribac curryhowardapproachtochurchssynthesis |