Skip to content
Navigation Menu
Sign in
Appearance settings
Platform
AI CODE CREATION
GitHub Copilot
Write better code with AI
GitHub Copilot app
Direct agents from issue to merge
MCP Registry
Integrate external tools
DEVELOPER WORKFLOWS
Actions
Automate any workflow
Codespaces
Instant dev environments
Issues
Plan and track work
Code Review
Manage code changes
Code Quality
Enforce quality at merge
APPLICATION SECURITY
GitHub Advanced Security
Find and fix vulnerabilities
Code security
Secure your code as you build
Secret protection
Stop leaks before they start
EXPLORE
Why GitHub
Documentation
Blog
Changelog
Marketplace
View all features
Solutions
BY COMPANY SIZE
Enterprises
Small and medium teams
Startups
Nonprofits
BY USE CASE
App Modernization
DevSecOps
DevOps
CI/CD
View all use cases
BY INDUSTRY
Healthcare
Financial services
Manufacturing
Government
View all industries
View all solutions
Resources
EXPLORE BY TOPIC
AI
Software Development
DevOps
Security
View all topics
EXPLORE BY TYPE
Customer stories
Events & webinars
Ebooks & reports
Business insights
GitHub Skills
SUPPORT & SERVICES
Documentation
Customer support
Community forum
Trust center
Partners
View all resources
Open Source
COMMUNITY
GitHub Sponsors
Fund open source developers
PROGRAMS
Security Lab
Maintainer Community
Accelerator
GitHub Stars
Archive Program
REPOSITORIES
Topics
Trending
Collections
Enterprise
ENTERPRISE SOLUTIONS
Enterprise platform
AI-powered developer platform
AVAILABLE ADD-ONS
GitHub Advanced Security
Enterprise-grade security features
Copilot for Business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Pricing
Type
/
to search
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
Uh oh!
There was an error while loading.
Please reload this page
.
DeepSpec
/
InteractionTrees
Public
Notifications
You must be signed in to change notification settings
Fork
60
Star
255
Code
Issues
22
Pull requests
9
Actions
Projects
Security and quality
0
Insights
Additional navigation options
Code
Issues
Pull requests
Actions
Projects
Security and quality
Insights
Support for the Prop Monad
- #165
#165
Open
YaZko
wants to merge 43 commits into
master
DeepSpec/InteractionTrees:master
from
prop
DeepSpec/InteractionTrees:prop
Copy head branch name to clipboard
Conversation
Commits
43
(43)
Checks
Files changed
Open
Support for the Prop Monad
#165
YaZko
wants to merge 43 commits into
master
DeepSpec/InteractionTrees:master
from
prop
DeepSpec/InteractionTrees:prop
Copy head branch name to clipboard
Commits
Commits on Mar 6, 2020
Quick draft after discussion with Irene
YaZko
committed
b2c404a
View commit details
Copy full SHA for b2c404a
Browse repository at this point
Commits on Mar 9, 2020
Working on the prop monad with Irene
YaZko
committed
e07d32e
View commit details
Copy full SHA for e07d32e
Browse repository at this point
Commits on Mar 17, 2020
WIP class for mayreturn
YaZko
committed
a7bed80
View commit details
Copy full SHA for a7bed80
Browse repository at this point
Monad laws for Kento
euisuny
committed
cb451db
View commit details
Copy full SHA for cb451db
Browse repository at this point
Commits on Mar 18, 2020
Left conjunction of left_unit proof PropTM
Kento Sugama
committed
30bb1be
View commit details
Copy full SHA for 30bb1be
Browse repository at this point
WIP ITree mayret proof
euisuny
committed
2a18bf1
View commit details
Copy full SHA for 2a18bf1
Browse repository at this point
The relationship between eutt and Returns is a bit tricky
YaZko
committed
aa93b5a
View commit details
Copy full SHA for aa93b5a
Browse repository at this point
Commits on Mar 19, 2020
WIP mayret_bind inversion case
euisuny
committed
f90c9c7
View commit details
Copy full SHA for f90c9c7
Browse repository at this point
bind_ret_l proof for PropTM
Kento Sugama
committed
a6e3728
View commit details
Copy full SHA for a6e3728
Browse repository at this point
started ret_bind_r
Kento Sugama
committed
27b9aa6
View commit details
Copy full SHA for 27b9aa6
Browse repository at this point
Merge branch 'prop' of https://github.com/DeepSpec/InteractionTrees into prop
Kento Sugama
committed
df9e3b2
View commit details
Copy full SHA for df9e3b2
Browse repository at this point
right unit proof changes
Kento Sugama
committed
9704520
View commit details
Copy full SHA for 9704520
Browse repository at this point
ITree mayret bind inversion proved
euisuny
committed
2336957
View commit details
Copy full SHA for 2336957
Browse repository at this point
Merge branch 'prop' of https://github.com/DeepSpec/InteractionTrees into prop
Kento Sugama
committed
fee7e1e
View commit details
Copy full SHA for fee7e1e
Browse repository at this point
Generalizing a few inversion lemmas
YaZko
committed
704f404
View commit details
Copy full SHA for 704f404
Browse repository at this point
Generalized inversion lemma for bind
YaZko
committed
01ac024
View commit details
Copy full SHA for 01ac024
Browse repository at this point
Commits on Mar 20, 2020
Inversion lemma for binding Vis nodes proved
euisuny
committed
51bae6c
View commit details
Copy full SHA for 51bae6c
Browse repository at this point
ITree mayret correctness instance complete
euisuny
committed
627465c
View commit details
Copy full SHA for 627465c
Browse repository at this point
Deleting extraneous file
euisuny
committed
077f5c5
View commit details
Copy full SHA for 077f5c5
Browse repository at this point
StateT transformer for MayReturn is concerning
YaZko
committed
aeaccbf
View commit details
Copy full SHA for aeaccbf
Browse repository at this point
Commits on Mar 22, 2020
Excluded middle in right unit PropTM
Kento Sugama
committed
0aa496d
View commit details
Copy full SHA for 0aa496d
Browse repository at this point
Commits on Mar 23, 2020
Proved one direction of associativity, PropT monad laws
Kento Sugama
committed
8a3e2c3
View commit details
Copy full SHA for 8a3e2c3
Browse repository at this point
monday vellvm meeting
Kento Sugama
committed
a552671
View commit details
Copy full SHA for a552671
Browse repository at this point
Commits on Mar 24, 2020
ret_bind_r using a stronger monad law
YaZko
committed
3b1992d
View commit details
Copy full SHA for 3b1992d
Browse repository at this point
right unit proof for PropTM with stronger monad law
Kento Sugama
committed
3badd6b
View commit details
Copy full SHA for 3badd6b
Browse repository at this point
resolved conflict
Kento Sugama
committed
3290b01
View commit details
Copy full SHA for 3290b01
Browse repository at this point
Mix bag of iter stuff and monad laws stuff
YaZko
committed
270378d
View commit details
Copy full SHA for 270378d
Browse repository at this point
Merge branch 'prop' of github.com:DeepSpec/InteractionTrees into prop
YaZko
committed
edd556e
View commit details
Copy full SHA for edd556e
Browse repository at this point
Commits on Mar 25, 2020
Comments
YaZko
committed
1de7443
View commit details
Copy full SHA for 1de7443
Browse repository at this point
Progress in proving Iter Laws
Show description for e976e74
euisuny
committed
e976e74
View commit details
Copy full SHA for e976e74
Browse repository at this point
Merge branch 'prop' of https://github.com/DeepSpec/InteractionTrees into prop
euisuny
committed
550770a
View commit details
Copy full SHA for 550770a
Browse repository at this point
Commits on Mar 26, 2020
New definition of MonadIter instance for PropTM
euisuny
committed
ac87b87
View commit details
Copy full SHA for ac87b87
Browse repository at this point
Updated prop_iter and unfold_iter proof with new iter def
euisuny
committed
4e1301e
View commit details
Copy full SHA for 4e1301e
Browse repository at this point
Commits on Mar 27, 2020
Updated IterUnfold forward case for indexed iter
euisuny
committed
7d0e9cc
View commit details
Copy full SHA for 7d0e9cc
Browse repository at this point
Small comments on proving unfolditer
euisuny
committed
fa3476b
View commit details
Copy full SHA for fa3476b
Browse repository at this point
Commits on Mar 31, 2020
Used dinatural law to prove part of iter unfold
euisuny
committed
37b77e7
View commit details
Copy full SHA for 37b77e7
Browse repository at this point
Attempt at changing the mayret definition
Kento Sugama
committed
9900b54
View commit details
Copy full SHA for 9900b54
Browse repository at this point
Merge branch 'prop' of https://github.com/DeepSpec/InteractionTrees into prop
Kento Sugama
committed
00e3eb0
View commit details
Copy full SHA for 00e3eb0
Browse repository at this point
Some work on using the axiom of choice to prove the missing monad law
YaZko
committed
f9eefcc
View commit details
Copy full SHA for f9eefcc
Browse repository at this point
Merge branch 'prop' of github.com:DeepSpec/InteractionTrees into prop
YaZko
committed
299017d
View commit details
Copy full SHA for 299017d
Browse repository at this point
Commits on Apr 3, 2020
experimental generalization of eqm
Zdancewic
committed
425f1d9
View commit details
Copy full SHA for 425f1d9
Browse repository at this point
Commits on Apr 6, 2020
Exploring "Run" function for tmayret
Kento Sugama
committed
b2507a9
View commit details
Copy full SHA for b2507a9
Browse repository at this point
attempt to apply tmayret with run to statet
Kento Sugama
committed
6b6e176
View commit details
Copy full SHA for 6b6e176
Browse repository at this point
You can’t perform that action at this time.
Kento Sugama