|
A '''reversible programming language''' is designed to bridge the gap between the theoretical models of [[reversible computing]] and practical [[software development]]. They provide constructs that allow programmers to write [[source code |code]] that is guaranteed, by the language's [[Syntax (programming languages)|syntax]] and [[Semantics (computer science)|semantics]], to be [[Execution (computing)|executable]] both forwards and backwards [[Deterministic system|deterministically]].
== Core concepts and design principles ==
The fundamental goal of a reversible programming language is to support computation that is deterministic in both the forward and backward directions. <ref name="Glück-2022.06.010">{{cite journal
| last1 = Glück
| first1 = Robert
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010 <!-- bibtex source: DBLP:journals/tcs/GluckY23 --> <!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
| url = https://doi.org/10.1016/j.tcs.2022.06.010
| doi-access= free
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
}}</ref> This is typically achieved by ensuring that every primitive operation and composite statement within the language is locally invertible.<ref name="Glück-2022.06.010"/> Local invertibility means that each basic computational step has a well-defined inverse, and the inverse of a sequence of steps is the sequence of inverse steps performed in reverse order.
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> This is typically achieved by ensuring that every primitive operation and composite statement within the language is locally invertible. <ref>{{cite journal
| last1 = Glück
| first1 = Robert
| last2 = Yokoyama
| first2 = Tetsuo
| title = Reversible computing from a programming language perspective
| journal = Theoretical Computer Science
| volume = 953
| article-number = 113429
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> Local invertibility means that each basic computational step has a well-defined inverse, and the inverse of a sequence of steps is the sequence of inverse steps performed in reverse order.
Key in the design of many reversible languages is cleanliness or garbage-free computation.<ref>{{cite arXiv
| editor-first2= Robert
| title = A Reversible Processor Architecture and Its Reversible Logic Design
| book-title = Reversible Computation - Third International Workshop, RC 2011, Gent, Belgium, July 4-54–5, 2011. Revised Papers
| series = Lecture Notes in Computer Science
| volume = 7165
| url = https://doi.org/10.1007/978-3-642-29517-1_3
| doi = 10.1007/978-3-642-29517-1_3
| id = {{DBLP|conf/rc/ThomsenAG11}} <!-- biburl: https://dblp.org/rec/conf/rc/ThomsenAG11.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Sun, 02 Jun 2019 21:17:32 +0200 -->
| id = {{DBLP|conf/rc/ThomsenAG11}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/rc/ThomsenAG11.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Sun, 02 Jun 2019 21:17:32 +0200 -->
}}</ref> Clean reversible languages aim to perform computations and their reversals using only the specified input and output variables.
To achieve local invertibility and cleanliness, reversible languages typically incorporate several features:
* '''Reversible Updates:''' Standard assignment statements (<code>x = expression</code>) are inherently irreversible because they overwrite and erase the previous value of x. Reversible languages replace these with reversible updates, often denoted using operators like <code>+=</code>, <code>-=</code>, <code>^=</code> (bitwise XOR).<ref name="Yokoyama-2010.02.007">{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}} <!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
| doi-access= free
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
}}</ref> An important restriction is that the variable being updated (e.g., x in <code>x += e</code>) must not appear in the expression on the right-hand side (e) to ensure the operation is bijective.<ref name="Yokoyama-2010.02.007"/> The swap operation (<code>x <=> y</code>), which exchanges the values of two variables, is another fundamental reversible update.<ref name="Choudhury">{{cite web
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> An important restriction is that the variable being updated (e.g., x in <code>x += e</code>) must not appear in the expression on the right-hand side (e) to ensure the operation is bijective.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> The swap operation (<code>x <=> y</code>), which exchanges the values of two variables, is another fundamental reversible update.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf <!-- If it were accessible online, you'd add: |url=... |access-date=... --> <!-- If it were for a specific institution, you could add: |institution=... -->
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* '''Reversible Control Flow:''' Conventional control flow structures like [[If-then-else]] and [[While loop]]s merge computational paths, making them irreversible. Reversible languages introduce specialized constructs. Conditionals often require both a test condition (evaluated on entry) and an assertion (a predicate that must hold true on exit from one branch and false on exit from the other).<ref name="Palazzo-2501.05259">{{cite arXiv
| last1 = Palazzo
| first1 = Matteo
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref name="Yokoyama-2010.02.007"/> These additional predicates store the necessary information to determine the execution path uniquely during backward execution, where the roles of tests and assertions are typically swapped.<ref name="Palazzo-2501.05259"/> This explicit management of control flow information is a significant difference from conventional programming.
}}</ref> Similarly, loops might require entry assertions and exit tests.<ref>{{cite conference
* '''Procedure Calls:''' Languages need mechanisms to invoke procedures both forwards and backwards. This is often achieved through paired commands like <code>call</code> (forward execution) and <code>uncall</code> or <code>rcall</code> (backward execution).<ref name="Choudhury"/>
| last1 = Yokoyama
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref name="Yokoyama-2010.02.007"/> Handling dynamic data structures like stacks requires careful semantic design to maintain reversibility, such as assuming variables are zero-cleared before being pushed onto a stack, ensuring <code>pop</code> can perfectly reverse <code>push</code>.<ref name="Choudhury"/> More recent research has explored reversible object-oriented features, including user-defined types, inheritance, and polymorphism.<ref>{{cite conference
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> These additional predicates store the necessary information to determine the execution path uniquely during backward execution, where the roles of tests and assertions are typically swapped.<ref>{{cite arXiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> This explicit management of control flow information is a significant difference from conventional programming.
* '''Procedure Calls:''' Languages need mechanisms to invoke procedures both forwards and backwards. This is often achieved through paired commands like <code>call</code> (forward execution) and <code>uncall</code> or <code>rcall</code> (backward execution).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* '''Data Structures:''' Early reversible languages often restricted data types to simple ones like integers and fixed-size arrays.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Handling dynamic data structures like stacks requires careful semantic design to maintain reversibility, such as assuming variables are zero-cleared before being pushed onto a stack, ensuring <code>pop</code> can perfectly reverse <code>push</code>.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> More recent research has explored reversible object-oriented features, including user-defined types, inheritance, and polymorphism.<ref>{{cite conference
| last1 = Haulund
| first1 = Tue
| editor-first2= Hafizur
| title = Implementing Reversible Object-Oriented Language Features on Reversible Machines
| book-title = Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-76–7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| url = https://doi.org/10.1007/978-3-319-59936-6_5
| doi = 10.1007/978-3-319-59936-6_5
| id = {{DBLP|conf/rc/HaulundMG17}} <!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
| id = {{DBLP|conf/rc/HaulundMG17}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
}}</ref>
* '''Computational Power:''' A common benchmark for the power of a reversible language is [[Turing completeness|r-Turing completeness]], which means the language can simulate any Reversible Turing Machine cleanly (without garbage accumulation).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* '''Computational Power:''' A common benchmark for the power of a reversible language is [[Turing completeness|r-Turing completeness]], which means the language can simulate any Reversible Turing Machine cleanly (without garbage accumulation).<ref name="Choudhury"/>
== Janus Language ==
[[Janus (time-reversible computing programming language)|Janus]] is widely recognized as the first structured, imperative programming language designed explicitly for reversible computation.<ref name="Yokoyama-2010.02.007"/>{{cite conferenceOriginally conceived by Christopher Lutz and Howard Derby at [[Caltech]] in the 1980s,<ref name="Choudhury"/> it was later rediscovered, formalized, and extended, notably by Tetsuo Yokoyama and Robert Glück.<ref name="Choudhury"/>
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Originally conceived by Christopher Lutz and Howard Derby at Caltech in the 1980s<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>, it was later rediscovered, formalized, and extended, notably by Tetsuo Yokoyama and Robert Glück.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
===Design philosophy===
Janus embodies the principle of local invertibility. It operates on a global store of variables (no heap allocation or local procedure scope in early versions) and ensures that every statement has a unique inverse.<ref>{{cite webname="Choudhury"/>
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
===Syntax and semantics===
* ''Program Structure:'' A Janus program consists of global variable declarations followed by procedure declarations. The execution starts at a procedure named <code>main</code>, or the last procedure defined if <code>main</code> is absent.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
* ''Data Types:'' Janus primarily uses 32-bit integers (interpreters may differ on signed vs. unsigned) and one-dimensional integer arrays of fixed size.<ref name="Yokoyama-2010.02.007"/>{{cite conferenceSome versions include stacks.<ref name="Yokoyama-2010.02.007"/> All variables and array elements are initialized to zero.<ref name="Yokoyama-2010.02.007"/>
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> Some versions include stacks.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> All variables and array elements are initialized to zero.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
* ''Statements:''
** '''Assignment:''' Reversible updates <code>x op= e</code> or <code>x[e] op= e</code>, where <code>op</code> is <code>+</code>, <code>-</code>, or <code>^</code> (bitwise XOR). The variable <code>x</code> must not appear in the expression <code>e</code>.<ref>{{cite conferencename="Yokoyama-2010.02.007"/>
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.
| last1 = Yokoyama
** '''Conditional:''' <code>if e1 then s1 else s2 fi e2</code>. The expression <code>e1</code> is the test evaluated upon forward entry. The expression <code>e2</code> is an assertion evaluated upon forward exit; it must be true if <code>s1</code> was executed and false if <code>s2</code> was executed. For backward execution (e.g., via <code>uncall</code>), <code>e2</code> acts as the test to determine which inverse branch (s1<sup>−1</sup> or s2<sup>−1</sup>) to take, and <code>e1</code> becomes the assertion checked upon exiting backward.<ref name="Palazzo-2501.05259"/>
| first1 = Tetsuo
** '''Loop:''' <code>from e1 do s1 loop s2 until e2</code>. Upon forward entry, assertion <code>e1</code> must be true. <code>s1</code> is executed. Then, test <code>e2</code> is evaluated. If true, the loop terminates. If false, <code>s2</code> is executed, after which assertion <code>e1</code> must now be false for the loop to continue back to <code>s1</code>. In reverse, <code>e2</code> is the entry assertion, s2<sup>−1</sup> is executed, <code>e1</code> is the test (loop continues if false, terminates if true), and s1<sup>−1</sup> is executed if the loop continues.<ref name="Yokoyama-2010.02.007"/>
| editor-last1 = Ulidowski
** '''Stack Operations:''' <code>push(x, stack)</code> and <code>pop(x, stack)</code>. Reversibility often relies on assumptions about the state of <code>x</code> (e.g., <code>x</code> must be 0 before <code>push</code> so <code>pop</code> can restore it).<ref name="Yokoyama-2010.02.007"/>** '''Local Variables:''' <code>local t x = e in s delocal t x = e</code> This block introduces a local variable <code>x</code>, initializes it reversibly using <code>e</code>, executes <code>s</code>, and then uncomputes <code>x</code> back to its initial state (usually 0) using the inverse of <code>e</code> upon exit.<ref name="Yokoyama-2010.02.007"/>
| editor-first1= Irek
** '''Procedure Call:''' <code>call id</code> executes procedure <code>id</code> forwards; <code>uncall id</code> executes procedure <code>id</code> backwards.<ref name="Choudhury"/> Procedures operate via side effects on the global store.
| title = Reversible Computation and Reversible Programming Languages
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
** '''Sequence:''' <code>s1; s2</code>. The inverse is <code>s2<sup>−1</sup>; s1<sup>−1</sup></code>.
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Swap:''' <code>x <=> y</code> exchanges the values of <code>x</code> and <code>y</code>.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
** '''Conditional:''' <code>if e1 then s1 else s2 fi e2</code>. The expression <code>e1</code> is the test evaluated upon forward entry. The expression <code>e2</code> is an assertion evaluated upon forward exit; it must be true if <code>s1</code> was executed and false if <code>s2</code> was executed. For backward execution (e.g., via <code>uncall</code>), <code>e2</code> acts as the test to determine which inverse branch (s1<sup>−1</sup> or s2<sup>−1</sup>) to take, and <code>e1</code> becomes the assertion checked upon exiting backward.<ref>{{cite arXiv
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref>
** '''Loop:''' <code>from e1 do s1 loop s2 until e2</code>. Upon forward entry, assertion <code>e1</code> must be true. <code>s1</code> is executed. Then, test <code>e2</code> is evaluated. If true, the loop terminates. If false, <code>s2</code> is executed, after which assertion <code>e1</code> must now be false for the loop to continue back to <code>s1</code>. In reverse, <code>e2</code> is the entry assertion, s2<sup>−1</sup> is executed, <code>e1</code> is the test (loop continues if false, terminates if true), and s1<sup>−1</sup> is executed if the loop continues.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Stack Operations:''' <code>push(x, stack)</code> and <code>pop(x, stack)</code>. Reversibility often relies on assumptions about the state of <code>x</code> (e.g., <code>x</code> must be 0 before <code>push</code> so <code>pop</code> can restore it).<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Local Variables:''' <code>local t x = e in s delocal t x = e</code> This block introduces a local variable <code>x</code>, initializes it reversibly using <code>e</code>, executes <code>s</code>, and then uncomputes <code>x</code> back to its initial state (usually 0) using the inverse of <code>e</code> upon exit.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>
** '''Procedure Call:''' <code>call id</code> executes procedure <code>id</code> forwards; <code>uncall id</code> executes procedure <code>id</code> backwards.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> Procedures operate via side effects on the global store.
** '''Skip:''' <code>skip</code> does nothing and is its own inverse.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
** '''Sequence:''' <code>s1; s2</code>. The inverse is <code>s2<sup>−1</sup>; s1<sup>−1</sup></code>.<ref>{{cite web |url=https://en.wikipedia.org/wiki/Janus_(time-reversible_computing_programming_language) |title=Janus (time-reversible computing programming language) |website=Wikipedia |access-date=April 9, 2025}}</ref>
===Implementations and code examples===
Several online interpreters for Janus exist.<ref>{{cite web |url=https://topps.diku.dk/pirc/?id=janus |title=Janus: a reversible imperative programming language |website=University of Copenhagen (DIKU) |access-date=April 9, 2025}}</ref> Janus has been used to implement various algorithms reversibly, including computing Fibonacci pairs,<ref name="Yokoyama-2010.02.007"/> simulating RTMs,<ref name="Yokoyama-2010.02.007"/> Fast Fourier Transform (FFT),<ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref> graph algorithms,<ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref> and simulating the Schrödinger wave equation.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>, simulating RTMs<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref>, Fast Fourier Transform (FFT)<ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref>, graph algorithms <ref>{{cite web |url=https://cra.org/ccc/wp-content/uploads/sites/2/2020/11/Jayson-Lynch_ReversibleAlgorithmsTalk.pdf |title=Reversible Algorithms |website=Computing Research Association |access-date=April 9, 2025}}</ref>, and simulating the Schrödinger wave equation.<ref>{{cite conference
| last1 = Yokoyama
| first1 = Tetsuo
| editor-first2= Eelco
| title = A reversible programming language and its invertible self-interpreter
| book-title = Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2007, Nice, France, January 15-1615–16, 2007
| pages = 144–153
| publisher = ACM
| url = https://doi.org/10.1145/1244381.1244404
| doi = 10.1145/1244381.1244404
| id = {{DBLP|conf/pepm/YokoyamaG07}} <!-- biburl: https://dblp.org/rec/conf/pepm/YokoyamaG07.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Sun, 02 Jun 2019 21:16:05 +0200 -->
| id = {{DBLP|conf/pepm/YokoyamaG07}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/pepm/YokoyamaG07.bib -->
}}</ref>
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Sun, 02 Jun 2019 21:16:05 +0200 -->
}}</ref>
The following fibpair procedure in Janus calculates a pair of consecutive Fibonacci numbers.<ref name="Glück-2022.06.010"/>{{cite journalGiven an input <code>n</code>, it sets <code>x1</code> to <code>F(n)</code> and <code>x2</code> to <code>F(n+1)</code>, assuming <code>x1</code> and <code>x2</code> are initially <code>0</code>:
| last1 = Glück
| first1 = Robert
| last2 = Yokoyama
| first2 = Tetsuo
| title = Reversible computing from a programming language perspective
| journal = Theoretical Computer Science
| volume = 953
| article-number = 113429
| year = 2023
| doi = 10.1016/j.tcs.2022.06.010
| url = https://doi.org/10.1016/j.tcs.2022.06.010
<!-- bibtex source: DBLP:journals/tcs/GluckY23 -->
<!-- biburl: https://dblp.org/rec/journals/tcs/GluckY23.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 22:24:24 +0100 -->
}}</ref> Given an input <code>n</code>, it sets <code>x1</code> to <code>F(n)</code> and <code>x2</code> to <code>F(n+1)</code>, assuming <code>x1</code> and <code>x2</code> are initially <code>0</code>:
<pre>
procedure main_fwd
n += 4
call fibpair
prodecure main_bwd
== R Language (MIT) ==
The R language (distinct from the [[R (programming language)|statistical language R]]) was developed by Michael P. Frank at [[MIT]] in the late 1990s as part of the Reversible Computing project.<ref name="Choudhury"/>{{cite webIt is an imperative, compiled language featuring an S-expression (Lisp-like) syntax.<ref name="Choudhury"/> A key aspect of R's design was its close integration with hardware development; it was designed to target the Pendulum reversible instruction set architecture (PISA), developed concurrently at MIT for an adiabatic CMOS processor.<ref name="Choudhury"/>
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> It is an imperative, compiled language featuring an S-expression (Lisp-like) syntax.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> A key aspect of R's design was its close integration with hardware development; it was designed to target the Pendulum reversible instruction set architecture (PISA), developed concurrently at MIT for an adiabatic CMOS processor.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
===Syntax and semantics===
* ''Program Structure:'' Programs are defined using <code>(defmain ...)</code> for the main routine and <code>(defsub ...)</code> for subroutines. Global variables and arrays are declared with <code>(defword ...)</code> and <code>(defarray ...)</code>.<ref>{{cite webname="Choudhury"/>
* ''Data Types:'' R primarily supports integers and integer arrays.<ref name="Choudhury"/>
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* ''Data Types:'' R primarily supports integers and integer arrays.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
* ''Statements:''
** '''Assignment/Update:''' Includes increment (<code>loc ++</code>), negation (<code>- loc</code>), swap (<code>loc <-> loc</code>), and reversible updates (<code>loc op= e</code>) using operators like <code>+=</code>, <code>-=</code>, <code>^=</code>, and specialized comparison-updates (<code><=<</code>, <code>>=></code>).<ref name="Choudhury"/>{{cite webSimilar restrictions to Janus apply regarding variable dependencies.
** '''Conditional:''' <code>(if e then s*)</code>. To ensure reversibility, the language requires that the value of the conditional expression <code>e</code> must be the same before and after the execution of the <code>then</code> block (<code>s*</code>).<ref name="Choudhury"/> This acts as an implicit invariant assertion, similar in function to Janus's explicit exit assertion.
| last1 = Choudhury
** '''Loop:''' <code>(for name = e_start to e_end s*)</code>. Reversibility requires that the loop iteration variable (<code>name</code>) must have the same value before entering and after exiting the loop.<ref name="Choudhury"/>
| first1 = Vikraman
** '''Local Binding:''' <code>(let ((name <- e)) s*)</code>. Introduces a local variable <code>name</code> initialized with <code>e</code>. Reversibility is ensured by requiring the variable to be returned to a known state (e.g., zero-cleared) before the scope is exited, analogous to Janus's <code>local/delocal</code>.<ref name="Choudhury"/>
| title = Reversible Programming Languages
** '''Procedure Call:''' Explicit forward <code>(call subname e*)</code> and reverse <code>(rcall subname e*)</code> calls are provided.<ref name="Choudhury"/>
| date = April 2018
** '''Output:''' <code>(printword e)</code> and <code>(println)</code> are included for output.<ref name="Choudhury"/> These are inherently irreversible operations.
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> Similar restrictions to Janus apply regarding variable dependencies.
** '''Conditional:''' <code>(if e then s*)</code>. To ensure reversibility, the language requires that the value of the conditional expression <code>e</code> must be the same before and after the execution of the <code>then</code> block (<code>s*</code>).<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> This acts as an implicit invariant assertion, similar in function to Janus's explicit exit assertion.
** '''Loop:''' <code>(for name = e_start to e_end s*)</code>. Reversibility requires that the loop iteration variable (<code>name</code>) must have the same value before entering and after exiting the loop.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Local Binding:''' <code>(let ((name <- e)) s*)</code>. Introduces a local variable <code>name</code> initialized with <code>e</code>. Reversibility is ensured by requiring the variable to be returned to a known state (e.g., zero-cleared) before the scope is exited, analogous to Janus's <code>local/delocal</code>.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Procedure Call:''' Explicit forward <code>(call subname e*)</code> and reverse <code>(rcall subname e*)</code> calls are provided.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** '''Output:''' <code>(printword e)</code> and <code>(println)</code> are included for output.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> These are inherently irreversible operations.
===Pendulum/PISA target architecture===
<!-- timestamp: Wed, 04 May 2022 12:58:38 +0200 -->
}}</ref>
* ''Architecture:'' Pendulum is a 12-bit, [[RISC]]-inspired, fully reversible microprocessor implemented in 0.5 µm CMOS.<ref>{{cite thesis
| last1 = Vieri
| first1 = Carlin
}}</ref>
* ''PISA Features:'' The instruction set includes several features tailored for reversibility:
** A Direction Bit (DIR) register tracks forward/backward execution mode.<ref>{{cite webname="Choudhury"/>
** A Branch Bit (BR) register assists with reversible control flow.<ref name="Choudhury"/>
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** A Branch Bit (BR) register assists with reversible control flow.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** Branch instructions (e.g., <code>BEZ</code>, <code>BLTZ</code>) are conditional and require careful pairing. Reverse branches (<code>RBEZ</code>, <code>RBLTZ</code>) also toggle the DIR bit.<ref>{{cite thesis
| last1 = Vieri
<!-- timestamp: Wed, 04 May 2022 12:58:32 +0200 -->
}}</ref>
** Memory access uses a reversible <code>EXCH</code> (exchange) instruction that swaps register and memory contents.<ref>{{cite webname="Choudhury"/>
** Arithmetic and logic instructions (e.g., <code>ADD</code>, <code>ANDX</code>, <code>XOR</code>, <code>SLLX</code>, <code>RL</code>) are designed to be reversible, with some operations' behavior (like addition/subtraction or rotation direction) dependent on the DIR bit.<ref name="Choudhury"/>
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
** Arithmetic and logic instructions (e.g., <code>ADD</code>, <code>ANDX</code>, <code>XOR</code>, <code>SLLX</code>, <code>RL</code>) are designed to be reversible, with some operations' behavior (like addition/subtraction or rotation direction) dependent on the DIR bit.<ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>
===Code examples===
The following PISA assembly code<ref>{{cite conference
| editor-first3= Andrei
| title = Reversible Machine Code and Its Abstract Processor Architecture
| book-title = Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-73–7, 2007, Proceedings
| series = Lecture Notes in Computer Science
| volume = 4649
| url = https://doi.org/10.1007/978-3-540-74510-5_9
| doi = 10.1007/978-3-540-74510-5_9
| id = {{DBLP|conf/csr/AxelsenGY07}} <!-- biburl: https://dblp.org/rec/conf/csr/AxelsenGY07.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 03 Mar 2025 21:01:20 +0100 -->
| id = {{DBLP|conf/csr/AxelsenGY07}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/csr/AxelsenGY07.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:01:20 +0100 -->
}}</ref> simulates a free-falling object. It includes a main section to call and "uncall" (reverse) a subroutine named Fall, which contains the core simulation logic.
| url = https://doi.org/10.4204/EPTCS.351.10
| doi = 10.4204/EPTCS.351.10
| id = {{DBLP|journals/corr/abs-2105-09929}} <!-- biburl: https://dblp.org/rec/journals/corr/abs-2105-09929.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 03 Mar 2025 21:31:45 +0100 -->
| arxiv= 2105.09929
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2105-09929.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:31:45 +0100 -->
}}</ref>
* '''ROOPL:''' The first reversible object-oriented programming language.<ref>{{cite conference
| editor-first2= Hafizur
| title = Implementing Reversible Object-Oriented Language Features on Reversible Machines
| book-title = Reversible Computation - 9th International Conference, RC 2017, Kolkata, India, July 6-76–7, 2017, Proceedings
| series = Lecture Notes in Computer Science
| volume = 10301
| url = https://doi.org/10.1007/978-3-319-59936-6_5
| doi = 10.1007/978-3-319-59936-6_5
| id = {{DBLP|conf/rc/HaulundMG17}} <!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
| id = {{DBLP|conf/rc/HaulundMG17}}
| url-access= subscription
<!-- biburl: https://dblp.org/rec/conf/rc/HaulundMG17.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 22 Oct 2019 15:21:14 +0200 -->
}}</ref> It extends the imperative reversible paradigm with features like user-defined data types (classes), inheritance, and subtype polymorphism.<ref>{{cite arXiv
| last1 = Haulund
| class = cs.PL
}}</ref>
* '''Flowchart Languages:''' Languages like R-CORE, R-WHILE, and SRL provide structured representations of reversible control flow, often serving as intermediate languages or theoretical models.<ref name="Palazzo-2501.05259"/> Their semantics can also be captured using categorical frameworks.<ref>{{cite arXivconference
| last1 = Palazzo
| first1 = Matteo
| last2 = Roversi
| first2 = Luca
| title = Reversible Computation with Stacks and "Reversible Management of Failures"
| eprint = 2501.05259
| year = 2025
<!-- biburl: https://dblp.org/rec/journals/corr/abs-2501-05259.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Wed, 19 Feb 2025 21:19:08 +0100 -->
| class = cs.PL
}}</ref> Their semantics can also be captured using categorical frameworks.<ref>{{cite conference
| last1 = Glück
| first1 = Robert
| editor-first1= Sam
| title = A Categorical Foundation for Structured Reversible Flowchart Languages
| book-title = Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-96–9, 2018
| series = Electronic Notes in Theoretical Computer Science
| volume = 341
| url = https://doi.org/10.1016/j.entcs.2018.03.021
| doi = 10.1016/J.ENTCS.2018.03.021
| id = {{DBLP|journals/entcs/GluckK18}} <!-- biburl: https://dblp.org/rec/journals/entcs/GluckK18.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 03 Feb 2020 15:57:36 +0100 -->
<!-- biburl: https://dblp.org/rec/journals/entcs/GluckK18.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Feb 2020 15:57:36 +0100 -->
}}</ref>
* '''Other Languages:''' A variety of other languages have been proposed, including Psi-Lisp ,<ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}} <!-- bibtex source: DBLP:journals/jfp/MatsudaW24 --> <!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</ref> Pi/Pi^o,<ref name="Choudhury"/> Inv,<ref>{{cite journal
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Pi/Pi^o <ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref>, Inv <ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}} <!-- bibtex source: DBLP:journals/jfp/MatsudaW24 --> <!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</ref> Yarel,<ref>{{cite arXiv
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Yarel <ref>{{cite arXiv
| last1 = Grandi
| first1 = Claudio
<!-- timestamp: Tue, 21 May 2019 18:03:37 +0200 -->
| class = cs.PL
}}</ref>, SPARCL ,<ref>{{cite journal
| last1 = Matsuda
| first1 = Kazutaka
| doi = 10.1017/S0956796823000126
| url = https://doi.org/10.1017/s0956796823000126
| id = {{DBLP|journals/jfp/MatsudaW24}} <!-- bibtex source: DBLP:journals/jfp/MatsudaW24 --> <!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
| id = {{DBLP|journals/jfp/MatsudaW24}}
| doi-access= free
<!-- bibtex source: DBLP:journals/jfp/MatsudaW24 -->
}}</ref> Hermes (focused on cryptography),<ref>{{cite web |url=https://reversible-computation-2020.github.io/slides/day-1-session-2-torben-mogensen.pdf |title=Hermes: A Language for Lightweight Encryption |website=Reversible Computation (RC) Lecture |access-date=April 9, 2025}}</ref> and Revs (compiling F# subset to circuits).<ref>{{cite book
<!-- biburl: https://dblp.org/rec/journals/jfp/MatsudaW24.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 01 Apr 2024 11:15:35 +0200 -->
}}</ref>, Hermes (focused on cryptography) <ref>{{cite web |url=https://reversible-computation-2020.github.io/slides/day-1-session-2-torben-mogensen.pdf |title=Hermes: A Language for Lightweight Encryption |website=Reversible Computation (RC) Lecture |access-date=April 9, 2025}}</ref>, and Revs (compiling F# subset to circuits).<ref>{{cite book
| last1 = Amy
| first1 = Matthew
| series = Lecture Notes in Computer Science
| arxiv = 1603.01635
| year = 2016 <!-- biburl: https://dblp.org/rec/journals/corr/AmyRS16.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Tue, 17 Sep 2019 14:15:13 +0200 -->
| year = 2016
<!-- biburl: https://dblp.org/rec/journals/corr/AmyRS16.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Tue, 17 Sep 2019 14:15:13 +0200 -->
| volume = 10427
| pages = 3–21
| hdl = 11585/884503
| url = https://doi.org/10.1109/MITP.2021.3117920
| id = {{DBLP|journals/itpro/LaneseSUS22}} <!-- bibtex source: DBLP:journals/itpro/LaneseSUS22 --> <!-- biburl: https://dblp.org/rec/journals/itpro/LaneseSUS22.bib --> <!-- bibsource: dblp computer science bibliography, https://dblp.org --> <!-- timestamp: Fri, 01 Apr 2022 11:23:39 +0200 -->
| id = {{DBLP|journals/itpro/LaneseSUS22}}
| hdl-access= free
<!-- bibtex source: DBLP:journals/itpro/LaneseSUS22 -->
<!-- biburl: https://dblp.org/rec/journals/itpro/LaneseSUS22.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Fri, 01 Apr 2022 11:23:39 +0200 -->
}}</ref>
{| class="wikitable"
|+ Comparison of Reversible Programming Languages<ref name="Yokoyama-2010.02.007"/><ref name="Choudhury"/><ref>{{cite conferencearXiv
| last1 = Yokoyama
| first1 = Tetsuo
| editor-last1 = Ulidowski
| editor-first1= Irek
| title = Reversible Computation and Reversible Programming Languages
| book-title = Proceedings of the Workshop on Reversible Computation, RC@ETAPS 2009, York, UK, March 22, 2009
| series = Electronic Notes in Theoretical Computer Science
| volume = 253
| issue = 6
| pages = 71–81
| publisher = Elsevier
| year = 2010
| url = https://doi.org/10.1016/j.entcs.2010.02.007
| doi = 10.1016/J.ENTCS.2010.02.007
| id = {{DBLP|journals/entcs/Yokoyama10}}
<!-- biburl: https://dblp.org/rec/journals/entcs/Yokoyama10.bib -->
<!-- bibsource: dblp computer science bibliography, https://dblp.org -->
<!-- timestamp: Mon, 03 Mar 2025 21:37:52 +0100 -->
}}</ref> <ref>{{cite web
| last1 = Choudhury
| first1 = Vikraman
| title = Reversible Programming Languages
| date = April 2018
| url=https://vikraman.org/files/reversible-languages.pdf
<!-- If it were accessible online, you'd add: |url=... |access-date=... -->
<!-- If it were for a specific institution, you could add: |institution=... -->
}}</ref> <ref>{{cite arXiv
| last1 = Haulund
| first1 = Tue
== References ==
{{reflist}}
{{uncategorized|date=August 2025}}
| 